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


definition
let x be Real;
let IT be Complex_Sequence;
attr IT 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
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;
func InvShift r -> Complex_Sequence means :Def2: :: CFDIFF_1:def 2
for n being Nat holds it . n = 1 / (n + r);
existence
ex b1 being Complex_Sequence st
for n being Nat holds b1 . n = 1 / (n + r)
proof end;
uniqueness
for b1, b2 being Complex_Sequence st ( for n being Nat holds b1 . n = 1 / (n + r) ) & ( for n being Nat holds b2 . n = 1 / (n + r) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines InvShift CFDIFF_1:def 2 :
for r being Real
for b2 being Complex_Sequence holds
( b2 = InvShift r iff for n being Nat holds b2 . n = 1 / (n + r) );

theorem Th2: :: CFDIFF_1:2
for r being Real st 0 < r holds
InvShift r is convergent
proof end;

registration
let r be positive Real;
cluster InvShift r -> convergent ;
coherence
InvShift r is convergent
by Th2;
end;

theorem Th3: :: CFDIFF_1:3
for r being Real st 0 < r holds
lim (InvShift r) = 0
proof end;

registration
let r be positive Real;
cluster InvShift r -> non-zero 0 -convergent ;
coherence
( InvShift r is non-zero & InvShift r is 0 -convergent )
proof end;
end;

registration
cluster V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total non-zero 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 )
proof end;
end;

registration
cluster Function-like non-zero 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
;
end;

registration
cluster V1() 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
proof end;
end;

theorem :: CFDIFF_1:4
for seq being Complex_Sequence holds
( seq is constant iff for n, m being Nat holds seq . n = seq . m )
proof end;

theorem :: CFDIFF_1:5
for seq being Complex_Sequence
for Nseq being V42() sequence of NAT
for n being Nat holds (seq * Nseq) . n = seq . (Nseq . n)
proof end;

definition
let IT be PartFunc of COMPLEX,COMPLEX;
attr IT 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 ) );

registration
cluster V1() 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 )
proof end;
end;

definition
mode C_RestFunc is total RestFunc-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 for Element of K19(K20(COMPLEX,COMPLEX));
existence
ex b1 being PartFunc of COMPLEX,COMPLEX st
( b1 is total & b1 is linear )
proof end;
end;

definition
mode C_LinearFunc is total linear PartFunc of COMPLEX,COMPLEX;
end;

registration
let L1, L2 be C_LinearFunc;
cluster L1 + 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 )
proof end;
cluster L1 - 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 )
proof end;
end;

registration
let a be Complex;
let L be C_LinearFunc;
cluster a (#) 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 )
proof end;
end;

registration
let R1, R2 be C_RestFunc;
cluster R1 + 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 )
proof end;
cluster R1 - 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 )
proof end;
cluster R1 (#) 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 )
proof end;
end;

registration
let a be Complex;
let R be C_RestFunc;
cluster a (#) 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 )
proof end;
end;

registration
let L1, L2 be C_LinearFunc;
cluster L1 (#) 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 )
proof end;
end;

registration
let R be C_RestFunc;
let L be C_LinearFunc;
cluster R (#) 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 )
proof end;
cluster L (#) 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 )
proof end;
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 Complex
for g being Real 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 :: 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 Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) );
end;

:: deftheorem 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 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 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 Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) )
proof end;
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 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 Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) holds
b1 = b2
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 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 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 :: CFDIFF_1:def 8
for x being Complex st x in dom f holds
f is_differentiable_in x;
end;

:: deftheorem 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 :: CFDIFF_1:def 9
( X c= dom f & f | X is differentiable );
end;

:: deftheorem 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 by XBOOLE_1:1;

definition
let X be Subset of COMPLEX;
attr X is closed means :: CFDIFF_1:def 10
for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent holds
lim s1 in X;
end;

:: deftheorem 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 :: CFDIFF_1:def 11
X ` is closed ;
end;

:: deftheorem 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 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 Real st X = { y where y is Complex : |.(y - z0).| <= r } holds
X is closed
proof end;

registration
cluster V52() open for Element of K19(COMPLEX);
existence
ex b1 being Subset of COMPLEX st b1 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 b1 being PartFunc of COMPLEX,COMPLEX st
( dom b1 = X & ( for x being Complex st x in X holds
b1 /. x = diff (f,x) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of COMPLEX,COMPLEX st dom b1 = X & ( for x being Complex st x in X holds
b1 /. x = diff (f,x) ) & dom b2 = X & ( for x being Complex st x in X holds
b2 /. x = diff (f,x) ) holds
b1 = b2
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 b3 being PartFunc of COMPLEX,COMPLEX holds
( b3 = f `| X iff ( dom b3 = X & ( for x being 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 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-zero
proof end;
end;

registration
let h be non-zero 0 -convergent Complex_Sequence;
let n be Nat;
cluster h ^\ n -> 0 -convergent for Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = h ^\ n holds
b1 is 0 -convergent
proof end;
end;

theorem Th18: :: CFDIFF_1:18
for k being 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 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 Nat
for seq being Complex_Sequence holds (seq ") ^\ k = (seq ^\ k) "
proof end;

theorem Th21: :: CFDIFF_1:21
for k being 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 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))) )
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
canceled;

::$CT
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_RestFunc st
( R /. 0c = 0c & R is_continuous_in 0c )
proof end;