:: Complex Function Differentiability :: by Chanapat Pacharapokin , Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura :: :: Received November 4, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin definition let x be real number ; let IT be Complex_Sequence; attrIT is x -convergent means :Def1: :: CFDIFF_1:def 1 ( IT is convergent & lim IT = x ); end; :: deftheorem Def1 defines -convergent CFDIFF_1:def_1_:_ for x being real number for IT being Complex_Sequence holds ( IT is x -convergent iff ( IT is convergent & lim IT = x ) ); theorem :: CFDIFF_1:1 for rs being Real_Sequence for cs being Complex_Sequence st rs = cs & rs is convergent holds cs is convergent ; definition let r be real number ; func InvShift r -> Complex_Sequence means :Def2: :: CFDIFF_1:def 2 for n being Element of NAT holds it . n = 1 / (n + r); existence ex b1 being Complex_Sequence st for n being Element of NAT holds b1 . n = 1 / (n + r) proofend; uniqueness for b1, b2 being Complex_Sequence st ( for n being Element of NAT holds b1 . n = 1 / (n + r) ) & ( for n being Element of NAT holds b2 . n = 1 / (n + r) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines InvShift CFDIFF_1:def_2_:_ for r being real number for b2 being Complex_Sequence holds ( b2 = InvShift r iff for n being Element of NAT holds b2 . n = 1 / (n + r) ); theorem Th2: :: CFDIFF_1:2 for r being real number st 0 < r holds InvShift r is convergent proofend; registration let r be real positive number ; cluster InvShift r -> convergent ; coherence InvShift r is convergent by Th2; end; theorem Th3: :: CFDIFF_1:3 for r being real number st 0 < r holds lim (InvShift r) = 0 proofend; registration let r be real positive number ; cluster InvShift r -> non-zero 0 -convergent ; coherence ( InvShift r is non-empty & InvShift r is 0 -convergent ) proofend; end; registration clusterV1() non-zero V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued 0 -convergent for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st ( b1 is 0 -convergent & b1 is non-zero ) proofend; end; registration cluster non-zero Function-like quasi_total 0 -convergent -> convergent for Element of K19(K20(NAT,COMPLEX)); coherence for b1 being Complex_Sequence st b1 is 0 -convergent & b1 is non-zero holds b1 is convergent by Def1; end; reconsider cs = NAT --> 0c as Complex_Sequence ; registration clusterV1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total quasi_total complex-valued for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st b1 is constant proofend; end; theorem :: CFDIFF_1:4 for seq being Complex_Sequence holds ( seq is constant iff for n, m being Element of NAT holds seq . n = seq . m ) proofend; theorem :: CFDIFF_1:5 for seq being Complex_Sequence for Nseq being V37() sequence of NAT for n being Element of NAT holds (seq * Nseq) . n = seq . (Nseq . n) proofend; definition let IT be PartFunc of COMPLEX,COMPLEX; attrIT is RestFunc-like means :Def3: :: CFDIFF_1:def 3 for h being non-zero 0 -convergent Complex_Sequence holds ( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ); end; :: deftheorem Def3 defines RestFunc-like CFDIFF_1:def_3_:_ for IT being PartFunc of COMPLEX,COMPLEX holds ( IT is RestFunc-like iff for h being non-zero 0 -convergent Complex_Sequence holds ( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) ); reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX ; registration clusterV1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued RestFunc-like for Element of K19(K20(COMPLEX,COMPLEX)); existence ex b1 being PartFunc of COMPLEX,COMPLEX st ( b1 is total & b1 is RestFunc-like ) proofend; end; definition mode C_RestFunc is total RestFunc-like PartFunc of COMPLEX,COMPLEX; end; definition let IT be PartFunc of COMPLEX,COMPLEX; attrIT is linear means :Def4: :: CFDIFF_1:def 4 ex a being Element of COMPLEX st for z being Element of COMPLEX holds IT /. z = a * z; end; :: deftheorem Def4 defines linear CFDIFF_1:def_4_:_ for IT being PartFunc of COMPLEX,COMPLEX holds ( IT is linear iff ex a being Element of COMPLEX st for z being Element of COMPLEX holds IT /. z = a * z ); registration clusterV1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued linear for Element of K19(K20(COMPLEX,COMPLEX)); existence ex b1 being PartFunc of COMPLEX,COMPLEX st ( b1 is total & b1 is linear ) proofend; end; definition mode C_LinearFunc is total linear PartFunc of COMPLEX,COMPLEX; end; registration let L1, L2 be C_LinearFunc; clusterL1 + L2 -> total linear for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 + L2 holds ( b1 is total & b1 is linear ) proofend; clusterL1 - L2 -> total linear for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 - L2 holds ( b1 is total & b1 is linear ) proofend; end; registration let a be Element of COMPLEX ; let L be C_LinearFunc; clustera (#) L -> total linear for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = a (#) L holds ( b1 is total & b1 is linear ) proofend; end; registration let R1, R2 be C_RestFunc; clusterR1 + R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 + R2 holds ( b1 is total & b1 is RestFunc-like ) proofend; clusterR1 - R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 - R2 holds ( b1 is total & b1 is RestFunc-like ) proofend; clusterR1 (#) R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 (#) R2 holds ( b1 is total & b1 is RestFunc-like ) proofend; end; registration let a be Element of COMPLEX ; let R be C_RestFunc; clustera (#) R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = a (#) R holds ( b1 is total & b1 is RestFunc-like ) proofend; end; registration let L1, L2 be C_LinearFunc; clusterL1 (#) L2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 (#) L2 holds ( b1 is total & b1 is RestFunc-like ) proofend; end; registration let R be C_RestFunc; let L be C_LinearFunc; clusterR (#) L -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R (#) L holds ( b1 is total & b1 is RestFunc-like ) proofend; clusterL (#) R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; coherence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L (#) R holds ( b1 is total & b1 is RestFunc-like ) ; end; definition let z0 be Complex; mode Neighbourhood of z0 -> Subset of COMPLEX means :Def5: :: CFDIFF_1:def 5 ex g being Real st ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= it ); existence ex b1 being Subset of COMPLEX ex g being Real st ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b1 ) proofend; end; :: deftheorem Def5 defines Neighbourhood CFDIFF_1:def_5_:_ for z0 being Complex for b2 being Subset of COMPLEX holds ( b2 is Neighbourhood of z0 iff ex g being Real st ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b2 ) ); theorem Th6: :: CFDIFF_1:6 for z0 being Element of COMPLEX for g being real number st 0 < g holds { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 proofend; theorem Th7: :: CFDIFF_1:7 for z0 being Element of COMPLEX for N being Neighbourhood of z0 holds z0 in N proofend; Lm1: for z0 being Complex for N1, N2 being Neighbourhood of z0 ex N being Neighbourhood of z0 st ( N c= N1 & N c= N2 ) proofend; definition let f be PartFunc of COMPLEX,COMPLEX; let z0 be Complex; predf is_differentiable_in z0 means :Def6: :: CFDIFF_1:def 6 ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ); end; :: deftheorem Def6 defines is_differentiable_in CFDIFF_1:def_6_:_ for f being PartFunc of COMPLEX,COMPLEX for z0 being Complex holds ( f is_differentiable_in z0 iff ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ); definition let f be PartFunc of COMPLEX,COMPLEX; let z0 be Complex; assume A1: f is_differentiable_in z0 ; func diff (f,z0) -> Element of COMPLEX means :Def7: :: CFDIFF_1:def 7 ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( it = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ); existence ex b1 being Element of COMPLEX ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( b1 = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) proofend; uniqueness for b1, b2 being Element of COMPLEX st ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( b1 = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) & ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( b2 = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines diff CFDIFF_1:def_7_:_ for f being PartFunc of COMPLEX,COMPLEX for z0 being Complex st f is_differentiable_in z0 holds for b3 being Element of COMPLEX holds ( b3 = diff (f,z0) iff ex N being Neighbourhood of z0 st ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st ( b3 = L /. 1r & ( for z being Element of COMPLEX st z in N holds (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) ); definition let f be PartFunc of COMPLEX,COMPLEX; attrf is differentiable means :Def8: :: CFDIFF_1:def 8 for x being Element of COMPLEX st x in dom f holds f is_differentiable_in x; end; :: deftheorem Def8 defines differentiable CFDIFF_1:def_8_:_ for f being PartFunc of COMPLEX,COMPLEX holds ( f is differentiable iff for x being Element of COMPLEX st x in dom f holds f is_differentiable_in x ); definition let f be PartFunc of COMPLEX,COMPLEX; let X be set ; predf is_differentiable_on X means :Def9: :: CFDIFF_1:def 9 ( X c= dom f & f | X is differentiable ); end; :: deftheorem Def9 defines is_differentiable_on CFDIFF_1:def_9_:_ for f being PartFunc of COMPLEX,COMPLEX for X being set holds ( f is_differentiable_on X iff ( X c= dom f & f | X is differentiable ) ); theorem Th8: :: CFDIFF_1:8 for X being set for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds X is Subset of COMPLEX proofend; definition let X be Subset of COMPLEX; attrX is closed means :Def10: :: CFDIFF_1:def 10 for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent holds lim s1 in X; end; :: deftheorem Def10 defines closed CFDIFF_1:def_10_:_ for X being Subset of COMPLEX holds ( X is closed iff for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent holds lim s1 in X ); definition let X be Subset of COMPLEX; attrX is open means :Def11: :: CFDIFF_1:def 11 X ` is closed ; end; :: deftheorem Def11 defines open CFDIFF_1:def_11_:_ for X being Subset of COMPLEX holds ( X is open iff X ` is closed ); theorem Th9: :: CFDIFF_1:9 for X being Subset of COMPLEX st X is open holds for z0 being Complex st z0 in X holds ex N being Neighbourhood of z0 st N c= X proofend; theorem :: CFDIFF_1:10 for X being Subset of COMPLEX st X is open holds for z0 being Complex st z0 in X holds ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X proofend; theorem Th11: :: CFDIFF_1:11 for X being Subset of COMPLEX st ( for z0 being Complex st z0 in X holds ex N being Neighbourhood of z0 st N c= X ) holds X is open proofend; theorem :: CFDIFF_1:12 for X being Subset of COMPLEX holds ( X is open iff for x being Complex st x in X holds ex N being Neighbourhood of x st N c= X ) by Th9, Th11; theorem Th13: :: CFDIFF_1:13 for X being Subset of COMPLEX for z0 being Element of COMPLEX for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| < r } holds X is open proofend; theorem :: CFDIFF_1:14 for X being Subset of COMPLEX for z0 being Element of COMPLEX for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| <= r } holds X is closed proofend; registration clusterV45() open for Element of K19(COMPLEX); existence ex b1 being Subset of COMPLEX st b1 is open proofend; end; theorem Th15: :: CFDIFF_1:15 for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX holds ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds f is_differentiable_in x ) ) ) proofend; theorem :: CFDIFF_1:16 for Y being Subset of COMPLEX for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on Y holds Y is open proofend; definition let f be PartFunc of COMPLEX,COMPLEX; let X be set ; assume A1: f is_differentiable_on X ; funcf `| X -> PartFunc of COMPLEX,COMPLEX means :Def12: :: CFDIFF_1:def 12 ( dom it = X & ( for x being Element of COMPLEX st x in X holds it /. x = diff (f,x) ) ); existence ex b1 being PartFunc of COMPLEX,COMPLEX st ( dom b1 = X & ( for x being Element of COMPLEX st x in X holds b1 /. x = diff (f,x) ) ) proofend; uniqueness for b1, b2 being PartFunc of COMPLEX,COMPLEX st dom b1 = X & ( for x being Element of COMPLEX st x in X holds b1 /. x = diff (f,x) ) & dom b2 = X & ( for x being Element of COMPLEX st x in X holds b2 /. x = diff (f,x) ) holds b1 = b2 proofend; end; :: deftheorem Def12 defines `| CFDIFF_1:def_12_:_ for f being PartFunc of COMPLEX,COMPLEX for X being set st f is_differentiable_on X holds for b3 being PartFunc of COMPLEX,COMPLEX holds ( b3 = f `| X iff ( dom b3 = X & ( for x being Element of COMPLEX st x in X holds b3 /. x = diff (f,x) ) ) ); theorem :: CFDIFF_1:17 for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom f & ex a1 being Element of COMPLEX st rng f = {a1} holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c ) ) proofend; registration let seq be non-zero Complex_Sequence; let k be Nat; clusterseq ^\ k -> non-zero ; coherence seq ^\ k is non-empty proofend; end; registration let h be non-zero 0 -convergent Complex_Sequence; let n be Element of NAT ; clusterh ^\ n -> 0 -convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = h ^\ n holds b1 is 0 -convergent proofend; end; theorem Th18: :: CFDIFF_1:18 for k being Element of NAT for seq, seq1 being Complex_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) proofend; theorem Th19: :: CFDIFF_1:19 for k being Element of NAT for seq, seq1 being Complex_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) proofend; theorem Th20: :: CFDIFF_1:20 for k being Element of NAT for seq being Complex_Sequence holds (seq ") ^\ k = (seq ^\ k) " proofend; theorem Th21: :: CFDIFF_1:21 for k being Element of NAT for seq, seq1 being Complex_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k) proofend; theorem Th22: :: CFDIFF_1:22 for f being PartFunc of COMPLEX,COMPLEX for x0 being Complex for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds for h being non-zero 0 -convergent Complex_Sequence for c being constant Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) proofend; theorem Th23: :: CFDIFF_1:23 for f1, f2 being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) proofend; theorem Th24: :: CFDIFF_1:24 for f1, f2 being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) proofend; theorem Th25: :: CFDIFF_1:25 for a being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX st f is_differentiable_in x0 holds ( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) ) proofend; theorem Th26: :: CFDIFF_1:26 for f1, f2 being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds ( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) ) proofend; theorem :: CFDIFF_1:27 for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom f & f | Z = id Z holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 1r ) ) proofend; theorem :: CFDIFF_1:28 for f1, f2 being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 + f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) proofend; theorem :: CFDIFF_1:29 for f1, f2 being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 - f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) proofend; theorem :: CFDIFF_1:30 for a being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom (a (#) f) & f is_differentiable_on Z holds ( a (#) f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds ((a (#) f) `| Z) /. x = a * (diff (f,x)) ) ) proofend; theorem :: CFDIFF_1:31 for f1, f2 being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom (f1 (#) f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds ( f1 (#) f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) ) proofend; theorem :: CFDIFF_1:32 for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom f & f | Z is constant holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = 0c ) ) proofend; theorem :: CFDIFF_1:33 for a, b being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Element of COMPLEX st x in Z holds f /. x = (a * x) + b ) holds ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds (f `| Z) /. x = a ) ) proofend; theorem Th34: :: CFDIFF_1:34 for f being PartFunc of COMPLEX,COMPLEX for x0 being Element of COMPLEX st f is_differentiable_in x0 holds f is_continuous_in x0 proofend; theorem :: CFDIFF_1:35 for X being set for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds f is_continuous_on X proofend; theorem :: CFDIFF_1:36 for X being set for f being PartFunc of COMPLEX,COMPLEX for Z being open Subset of COMPLEX st f is_differentiable_on X & Z c= X holds f is_differentiable_on Z proofend; theorem :: CFDIFF_1:37 canceled; theorem :: CFDIFF_1:38 for x0 being Element of COMPLEX for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_in x0 holds ex R being C_RestFunc st ( R /. 0c = 0c & R is_continuous_in 0c ) proofend;