CFDIFF_1: Complex Function Differentiability

:: 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 :

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);

proof end;

proof end;

end;

:: deftheorem Def2 defines InvShift CFDIFF_1:def 2 :

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 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 ;

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));

proof end;

end;

registration

cluster Function-like non-zero quasi_total 0 -convergent -> convergent for Element of K19(K20(NAT,COMPLEX));

end;

registration

cluster V1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total quasi_total complex-valued for Element of K19(K20(NAT,COMPLEX));

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 :

registration

cluster V1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued RestFunc-like for Element of K19(K20(COMPLEX,COMPLEX));

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 :

registration

cluster V1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued linear for Element of K19(K20(COMPLEX,COMPLEX));

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;

proof end;

cluster L1 - L2 -> total linear for PartFunc of COMPLEX,COMPLEX;

proof end;

end;

registration

let a be Complex;
let L be C_LinearFunc;

cluster a (#) L -> total linear for PartFunc of COMPLEX,COMPLEX;

proof end;

end;

registration

let R1, R2 be C_RestFunc;

cluster R1 + R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;

proof end;

cluster R1 - R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;

proof end;

cluster R1 (#) R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;

proof end;

end;

registration

let a be Complex;
let R be C_RestFunc;

cluster a (#) R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;

proof end;

end;

registration

let L1, L2 be C_LinearFunc;

cluster L1 (#) L2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;

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;

proof end;

cluster L (#) R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;

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 );

proof end;

end;

:: deftheorem Def5 defines Neighbourhood CFDIFF_1:def 5 :

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 :

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)) ) ) );

proof end;

proof end;

end;

:: deftheorem Def7 defines diff CFDIFF_1:def 7 :

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 :

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 :

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 :

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 :

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);

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) ) );

proof end;

proof end;

end;

:: deftheorem Def12 defines `| CFDIFF_1:def 12 :

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 ;

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;

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;