:: Complex Function Differentiability
:: by Chanapat Pacharapokin , Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura
::
:: Received November 4, 2008
:: Copyright (c) 2008-2011 Association of Mizar Users

begin

definition

let IT be Complex_Sequence;
attr IT is convergent_to_0 means :Def1: :: CFDIFF_1:def 1
( IT is non-empty & IT is convergent & lim IT = 0 );

end;

:: deftheorem Def1 defines convergent_to_0 CFDIFF_1:def 1 :
for IT being Complex_Sequence holds
( IT is convergent_to_0 iff ( IT is non-empty & IT is convergent & lim IT = 0 ) );

theorem :: CFDIFF_1:1

for rs being Real_Sequence
for cs being Complex_Sequence st rs = cs & rs is convergent holds
cs is convergent

proof end;

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 b₁ being Complex_Sequence st
for n being Element of NAT holds b₁ . n = 1 / (n + r)

proof end;

uniqueness
for b₁, b₂ being Complex_Sequence st ( for n being Element of NAT holds b₁ . n = 1 / (n + r) ) & ( for n being Element of NAT holds b₂ . n = 1 / (n + r) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines InvShift CFDIFF_1:def 2 :
for r being real number
for b₂ being Complex_Sequence holds
( b₂ = InvShift r iff for n being Element of NAT holds b₂ . n = 1 / (n + r) );

theorem Th2: :: CFDIFF_1:2

for r being real number st 0 < r holds
InvShift r is convergent

proof end;

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

proof end;

registration

let r be real positive number ;
cluster InvShift r -> convergent_to_0 ;
coherence
InvShift r is convergent_to_0

proof end;

end;

registration

cluster V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued convergent_to_0 Element of K21(K22(NAT,COMPLEX));
existence
ex b₁ being Complex_Sequence st b₁ is convergent_to_0

proof end;

end;

registration

cluster Function-like quasi_total convergent_to_0 -> non-zero convergent Element of K21(K22(NAT,COMPLEX));
coherence
for b₁ being Complex_Sequence st b₁ is convergent_to_0 holds
( b₁ is non-empty & b₁ is convergent ) by Def1;

end;

reconsider cs = NAT --> 0c as Complex_Sequence ;

registration

cluster V1() V4( NAT ) V5( COMPLEX ) Function-like V8() V11() total quasi_total complex-valued Element of K21(K22(NAT,COMPLEX));
existence
ex b₁ being Complex_Sequence st b₁ is constant

proof end;

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 )

proof end;

theorem :: CFDIFF_1:5

for seq being Complex_Sequence
for Nseq being V33() sequence of NAT
for n being Element of NAT holds (seq * Nseq) . n = seq . (Nseq . n)

proof end;

definition

let IT be PartFunc of COMPLEX,COMPLEX;
attr IT is REST-like means :Def3: :: CFDIFF_1:def 3
for h being convergent_to_0 Complex_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 );

end;

:: deftheorem Def3 defines REST-like CFDIFF_1:def 3 :
for IT being PartFunc of COMPLEX,COMPLEX holds
( IT is REST-like iff for h being convergent_to_0 Complex_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) );

reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX ;

registration

cluster V1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued REST-like Element of K21(K22(COMPLEX,COMPLEX));
existence
ex b₁ being PartFunc of COMPLEX,COMPLEX st
( b₁ is total & b₁ is REST-like )

proof end;

end;

definition

mode C_REST is total REST-like PartFunc of COMPLEX,COMPLEX;

end;

definition

let IT be PartFunc of COMPLEX,COMPLEX;
attr IT is linear means :Def4: :: CFDIFF_1:def 4
ex a being Complex st
for z being 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 Complex st
for z being Complex holds IT /. z = a * z );

registration

cluster V1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued linear Element of K21(K22(COMPLEX,COMPLEX));
existence
ex b₁ being PartFunc of COMPLEX,COMPLEX st
( b₁ is total & b₁ is linear )

proof end;

end;

definition

mode C_LINEAR is total linear PartFunc of COMPLEX,COMPLEX;

end;

registration

let L1, L2 be C_LINEAR;
cluster L1 + L2 -> total linear PartFunc of COMPLEX,COMPLEX;
coherence
for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = L1 + L2 holds
( b₁ is total & b₁ is linear )

proof end;

cluster L1 - L2 -> total linear PartFunc of COMPLEX,COMPLEX;
coherence
for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = L1 - L2 holds
( b₁ is total & b₁ is linear )

proof end;

end;

registration

let a be Complex;
let L be C_LINEAR;
cluster a (#) L -> total linear PartFunc of COMPLEX,COMPLEX;
coherence
for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = a (#) L holds
( b₁ is total & b₁ is linear )

proof end;

end;

registration

let R1, R2 be C_REST;
cluster R1 + R2 -> total REST-like PartFunc of COMPLEX,COMPLEX;
coherence
for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = R1 + R2 holds
( b₁ is total & b₁ is REST-like )

proof end;

cluster R1 - R2 -> total REST-like PartFunc of COMPLEX,COMPLEX;
coherence
for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = R1 - R2 holds
( b₁ is total & b₁ is REST-like )

proof end;

cluster R1 (#) R2 -> total REST-like PartFunc of COMPLEX,COMPLEX;
coherence
for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = R1 (#) R2 holds
( b₁ is total & b₁ is REST-like )

proof end;

end;

registration

let a be Complex;
let R be C_REST;
cluster a (#) R -> total REST-like PartFunc of COMPLEX,COMPLEX;
coherence
for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = a (#) R holds
( b₁ is total & b₁ is REST-like )

proof end;

end;

registration

let L1, L2 be C_LINEAR;
cluster L1 (#) L2 -> total REST-like PartFunc of COMPLEX,COMPLEX;
coherence
for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = L1 (#) L2 holds
( b₁ is total & b₁ is REST-like )

proof end;

end;

registration

let R be C_REST;
let L be C_LINEAR;
cluster R (#) L -> total REST-like PartFunc of COMPLEX,COMPLEX;
coherence
for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = R (#) L holds
( b₁ is total & b₁ is REST-like )

proof end;

cluster L (#) R -> total REST-like PartFunc of COMPLEX,COMPLEX;
coherence
for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = L (#) R holds
( b₁ is total & b₁ is REST-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 b₁ being Subset of COMPLEX ex g being Real st
( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b₁ )

proof end;

end;

:: deftheorem Def5 defines Neighbourhood CFDIFF_1:def 5 :
for z0 being Complex
for b₂ being Subset of COMPLEX holds
( b₂ is Neighbourhood of z0 iff ex g being Real st
( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b₂ ) );

theorem Th6: :: CFDIFF_1:6

for z0 being Complex
for g being real number st 0 < g holds
{ y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0

proof end;

theorem Th7: :: CFDIFF_1:7

for z0 being Complex
for N being Neighbourhood of z0 holds z0 in N

proof end;

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 )

proof end;

definition

let f be PartFunc of COMPLEX,COMPLEX;
let z0 be Complex;
pred f 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_LINEAR ex R being C_REST st
for z being 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_LINEAR ex R being C_REST st
for z being 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) -> Complex means :Def7: :: CFDIFF_1:def 7
ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LINEAR ex R being C_REST st
( it = L /. 1r & ( for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) );
existence
ex b₁ being Complex ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LINEAR ex R being C_REST st
( b₁ = L /. 1r & ( for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) )

proof end;

uniqueness
for b₁, b₂ being Complex st ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LINEAR ex R being C_REST st
( b₁ = L /. 1r & ( for z being 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_LINEAR ex R being C_REST st
( b₂ = L /. 1r & ( for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) holds
b₁ = b₂

proof end;

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 b₃ being Complex holds
( b₃ = diff (f,z0) iff ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LINEAR ex R being C_REST st
( b₃ = L /. 1r & ( for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) );

definition

let f be PartFunc of COMPLEX,COMPLEX;
attr f is differentiable means :Def8: :: CFDIFF_1:def 8
for x being 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 Complex st x in dom f holds
f is_differentiable_in x );

definition

let f be PartFunc of COMPLEX,COMPLEX;
let X be set ;
pred f 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

proof end;

definition

let X be Subset of COMPLEX;
attr X 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;
attr X 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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

registration

cluster V41() open Element of K21(COMPLEX);
existence
ex b₁ being Subset of COMPLEX st b₁ is open

proof end;

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 Complex st x in Z holds
f is_differentiable_in x ) ) )

proof end;

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

proof end;

definition

let f be PartFunc of COMPLEX,COMPLEX;
let X be set ;
assume A1: f is_differentiable_on X ;
func f `| X -> PartFunc of COMPLEX,COMPLEX means :Def12: :: CFDIFF_1:def 12
( dom it = X & ( for x being Complex st x in X holds
it /. x = diff (f,x) ) );
existence
ex b₁ being PartFunc of COMPLEX,COMPLEX st
( dom b₁ = X & ( for x being Complex st x in X holds
b₁ /. x = diff (f,x) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of COMPLEX,COMPLEX st dom b₁ = X & ( for x being Complex st x in X holds
b₁ /. x = diff (f,x) ) & dom b₂ = X & ( for x being Complex st x in X holds
b₂ /. x = diff (f,x) ) holds
b₁ = b₂

proof end;

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 b<sub>3</sub> being PartFunc of COMPLEX,COMPLEX holds
( b<sub>3</sub> = f `| X iff ( dom b₃ = X & ( for x being Complex st x in X holds
b₃ /. 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 Complex st rng f = {a1} holds
( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 0c ) )

proof end;

registration

let seq be non-zero Complex_Sequence;
let k be Nat;
cluster seq ^\ k -> non-zero ;
coherence
seq ^\ k is non-empty

proof end;

end;

registration

let h be convergent_to_0 Complex_Sequence;
let n be Element of NAT ;
cluster h ^\ n -> convergent_to_0 ;
coherence
h ^\ n is convergent_to_0

proof end;

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)

proof end;

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)

proof end;

theorem Th20: :: CFDIFF_1:20

for k being Element of NAT
for seq being Complex_Sequence holds (seq ") ^\ k = (seq ^\ k) "

proof end;

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)

proof end;

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 convergent_to_0 Complex_Sequence
for c being V8() 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))) )

proof end;

theorem Th23: :: CFDIFF_1:23

for f1, f2 being PartFunc of COMPLEX,COMPLEX
for x0 being 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)) )

proof end;

theorem Th24: :: CFDIFF_1:24

for f1, f2 being PartFunc of COMPLEX,COMPLEX
for x0 being 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)) )

proof end;

theorem Th25: :: CFDIFF_1:25

for a being Complex
for f being PartFunc of COMPLEX,COMPLEX
for x0 being Complex st f is_differentiable_in x0 holds
( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) )

proof end;

theorem Th26: :: CFDIFF_1:26

for f1, f2 being PartFunc of COMPLEX,COMPLEX
for x0 being 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))) )

proof end;

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 Complex st x in Z holds
(f `| Z) /. x = 1r ) )

proof end;

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 Complex st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )

proof end;

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 Complex st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )

proof end;

theorem :: CFDIFF_1:30

for a being 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 Complex st x in Z holds
((a (#) f) `| Z) /. x = a * (diff (f,x)) ) )

proof end;

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 Complex st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) )

proof end;

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 Complex st x in Z holds
(f `| Z) /. x = 0c ) )

proof end;

theorem :: CFDIFF_1:33

for a, b being Complex
for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Complex st x in Z holds
f /. x = (a * x) + b ) holds
( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = a ) )

proof end;

theorem Th34: :: CFDIFF_1:34

for f being PartFunc of COMPLEX,COMPLEX
for x0 being Complex st f is_differentiable_in x0 holds
f is_continuous_in x0

proof end;

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

proof end;

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

proof end;

theorem :: CFDIFF_1:37

for seq being Complex_Sequence st seq is convergent holds
|.seq.| is convergent ;

theorem :: CFDIFF_1:38

for x0 being Complex
for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_in x0 holds
ex R being C_REST st
( R /. 0c = 0c & R is_continuous_in 0c )

proof end;