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


Lm1: for seq being Real_Sequence
for cseq being Complex_Sequence
for rlim being Real st seq = cseq & seq is convergent & lim seq = rlim holds
lim cseq = rlim
proof end;

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

Lm3: for seq being Real_Sequence
for cseq being Complex_Sequence st seq = cseq holds
( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) )
proof end;

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;

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

Lm5: for seq, cseq being Complex_Sequence st cseq = <i> (#) seq holds
( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) )
proof end;

:: Cauchy-Riemann
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;

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

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

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

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

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

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

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

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

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

Lm15: for x, y being Real
for z being Complex st z = x + (y * <i>) holds
|.z.| <= |.x.| + |.y.|
proof end;

Lm16: for x, y being Real holds
( |.x.| <= |.(x + (y * <i>)).| & |.y.| <= |.(x + (y * <i>)).| )
proof end;

Lm17: for x, y being Real
for v being Element of (REAL-NS 2) st v = <*x,y*> holds
||.v.|| <= |.x.| + |.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;

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

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

Lm20: for x being Real
for vx being Element of (REAL-NS 1) st vx = <*x*> holds
||.vx.|| = |.x.|
proof end;

Lm21: for v being Element of (REAL-NS 1) holds |.((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;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

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;