:: Cauchy-Riemann Differential Equations of Complex Functions
:: by Hiroshi Yamazaki , Yasunari Shidama , Chanapat Pacharapokin and Yatsuka Nakamura
::
:: Received April 7, 2009
:: Copyright (c) 2009 Association of Mizar Users

Lm1: for seq being Real_Sequence
for cseq being Complex_Sequence st seq = cseq holds
( seq is convergent iff cseq is convergent )

proof end;

Lm2: for seq being Real_Sequence
for cseq being Complex_Sequence
for rlim being real number st seq = cseq & seq is convergent & lim seq = rlim holds
lim cseq = rlim

proof end;

Lm3: for seq being Real_Sequence
for cseq being Complex_Sequence
for rlim being Real st seq = cseq & cseq is convergent & lim cseq = rlim holds
lim seq = rlim

proof end;

Lm4: for seq being Real_Sequence
for cseq being Complex_Sequence st seq = cseq holds
( seq is convergent_to_0 iff cseq is convergent_to_0 )

proof end;

definition

let f be PartFunc of COMPLEX ,COMPLEX ;
func Re f -> PartFunc of COMPLEX ,REAL means :Def1: :: CFDIFF_2:def 1
( dom f = dom it & ( for z being Complex st z in dom it holds
it . z = Re (f /. z) ) );
existence
ex b₁ being PartFunc of COMPLEX ,REAL st
( dom f = dom b₁ & ( for z being Complex st z in dom b₁ holds
b₁ . z = Re (f /. z) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of COMPLEX ,REAL st dom f = dom b₁ & ( for z being Complex st z in dom b₁ holds
b₁ . z = Re (f /. z) ) & dom f = dom b₂ & ( for z being Complex st z in dom b₂ holds
b₂ . z = Re (f /. z) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Re CFDIFF_2:def 1 :

for f being PartFunc of COMPLEX ,COMPLEX
for b₂ being PartFunc of COMPLEX ,REAL holds
( b₂ = Re f iff ( dom f = dom b₂ & ( for z being Complex st z in dom b₂ holds
b₂ . z = Re (f /. z) ) ) );

definition

let f be PartFunc of COMPLEX ,COMPLEX ;
func Im f -> PartFunc of COMPLEX ,REAL means :Def2: :: CFDIFF_2:def 2
( dom f = dom it & ( for z being Complex st z in dom it holds
it . z = Im (f /. z) ) );
existence
ex b₁ being PartFunc of COMPLEX ,REAL st
( dom f = dom b₁ & ( for z being Complex st z in dom b₁ holds
b₁ . z = Im (f /. z) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of COMPLEX ,REAL st dom f = dom b₁ & ( for z being Complex st z in dom b₁ holds
b₁ . z = Im (f /. z) ) & dom f = dom b₂ & ( for z being Complex st z in dom b₂ holds
b₂ . z = Im (f /. z) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Im CFDIFF_2:def 2 :

for f being PartFunc of COMPLEX ,COMPLEX
for b₂ being PartFunc of COMPLEX ,REAL holds
( b₂ = Im f iff ( dom f = dom b₂ & ( for z being Complex st z in dom b₂ holds
b₂ . z = Im (f /. z) ) ) );

theorem Th1: :: CFDIFF_2:1

for f being PartFunc of COMPLEX ,COMPLEX st f is total holds
( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX )

proof end;

Lm5: for seq, cseq being Complex_Sequence st cseq = <i> (#) seq holds
( seq is non-zero iff cseq is non-zero )

proof end;

Lm6: for seq, cseq being Complex_Sequence st cseq = <i> (#) seq holds
( seq is convergent_to_0 iff cseq is convergent_to_0 )

proof end;

theorem Th2: :: CFDIFF_2:2

for f being PartFunc of COMPLEX ,COMPLEX
for u, v being PartFunc of (REAL 2),REAL
for z0 being Complex
for x0, y0 being Real
for xy0 being Element of REAL 2 st ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i> )) ) ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i> )) ) ) & z0 = x0 + (y0 * <i> ) & xy0 = <*x0,y0*> & f is_differentiable_in z0 holds
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff f,z0) = partdiff u,xy0,1 & Re (diff f,z0) = partdiff v,xy0,2 & Im (diff f,z0) = - (partdiff u,xy0,2) & Im (diff f,z0) = partdiff v,xy0,1 )

proof end;

Lm7: for x, y being Real
for vx, vy being Point of (REAL-NS 1) st vx = <*x*> & vy = <*y*> holds
( vx + vy = <*(x + y)*> & vx - vy = <*(x - y)*> )

proof end;

Lm8: for x, y, z, w being Real
for vx, vy being Element of REAL 2 st vx = <*x,y*> & vy = <*z,w*> holds
( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> )

proof end;

Lm9: for x, y, a being Real
for vx being Element of REAL 2 st vx = <*x,y*> holds
a * vx = <*(a * x),(a * y)*>

proof end;

Lm10: for x, y being Real holds <*x,y*> is Point of (REAL-NS 2)

proof end;

Lm11: for x, y, z, w being Real
for vx, vy being Point of (REAL-NS 2) st vx = <*x,y*> & vy = <*z,w*> holds
( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> )

proof end;

Lm12: for x, y, a being Real
for vx being Point of (REAL-NS 2) st vx = <*x,y*> holds
a * vx = <*(a * x),(a * y)*>

proof end;

Lm13: for u being PartFunc of (REAL 2),REAL
for xy being Element of REAL 2 st xy in dom u holds
(<>* u) . xy = <*(u . xy)*>

proof end;

Lm14: for u being PartFunc of (REAL 2),REAL
for x, y being Real st <*x,y*> in dom u holds
(<>* u) /. <*x,y*> = <*(u /. <*x,y*>)*>

proof end;

Lm15: for x, y being Real
for z being Complex
for v being Element of (REAL-NS 2) st z = x + (y * <i> ) & v = <*x,y*> holds
|.z.| = ||.v.||

proof end;

Lm16: for x, y being Real
for z being Complex st z = x + (y * <i> ) holds
|.z.| <= (abs x) + (abs y)

proof end;

Lm17: for x, y being Real holds
( abs x <= |.(x + (y * <i> )).| & abs y <= |.(x + (y * <i> )).| )

proof end;

Lm18: for x, y being Real
for v being Element of (REAL-NS 2) st v = <*x,y*> holds
||.v.|| <= (abs x) + (abs y)

proof end;

theorem Th3: :: CFDIFF_2:3

for seq being Real_Sequence holds
( seq is convergent & lim seq = 0 iff ( abs seq is convergent & lim (abs seq) = 0 ) )

proof end;

theorem Th4: :: CFDIFF_2:4

for X being RealNormSpace
for seq being sequence of X holds
( seq is convergent & lim seq = 0. X iff ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) )

proof end;

Lm19: for x being Real
for vx being Element of (REAL-NS 2) st vx = <*x,0 *> holds
||.vx.|| = abs x

proof end;

Lm20: for x being Real
for vx being Element of (REAL-NS 2) st vx = <*0 ,x*> holds
||.vx.|| = abs x

proof end;

Lm21: for x being Real
for vx being Element of (REAL-NS 1) st vx = <*x*> holds
||.vx.|| = abs x

proof end;

Lm22: for v being Element of (REAL-NS 1) holds abs ((proj 1,1) . v) = ||.v.||

proof end;

theorem Th5: :: CFDIFF_2:5

for u being PartFunc of (REAL 2),REAL
for x0, y0 being Real
for xy0 being Element of REAL 2 st xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 holds
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff u,xy0,1)*> = (diff (<>* u),xy0) . <*1,0 *> & <*(partdiff u,xy0,2)*> = (diff (<>* u),xy0) . <*0 ,1*> )

proof end;

theorem :: CFDIFF_2:6

for f being PartFunc of COMPLEX ,COMPLEX
for u, v being PartFunc of (REAL 2),REAL
for z0 being Complex
for x0, y0 being Real
for xy0 being Element of REAL 2 st ( for x, y being Real st <*x,y*> in dom v holds
x + (y * <i> ) in dom f ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i> )) ) ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i> )) ) ) & z0 = x0 + (y0 * <i> ) & xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff u,xy0,1 = partdiff v,xy0,2 & partdiff u,xy0,2 = - (partdiff v,xy0,1) holds
( f is_differentiable_in z0 & u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff f,z0) = partdiff u,xy0,1 & Re (diff f,z0) = partdiff v,xy0,2 & Im (diff f,z0) = - (partdiff u,xy0,2) & Im (diff f,z0) = partdiff v,xy0,1 )

proof end;