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

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, PARTFUN1, REAL_1, SEQ_1, COMSEQ_1, SEQ_2, CARD_1, FUNCT_1, COMPLEX1, RELAT_1, NAT_1, ORDINAL2, ARYTM_3, XXREAL_0, ARYTM_1, FDIFF_1, VALUED_0, XCMPLX_0, VALUED_1, FINSEQ_1, PDIFF_1, AFINSQ_1, CARD_3, RCOMP_1, TARSKI, CFDIFF_1, FUNCT_2, XXREAL_1, PRE_TOPC, REAL_NS1, BINOP_2, NORMSP_1, EUCLID, MCART_1, RVSUM_1, SQUARE_1, SUPINF_2, STRUCT_0, LOPBAN_1, FUNCT_7;
notations HIDDEN, TARSKI, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1, BINOP_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, BINOP_2, XREAL_0, COMPLEX1, REAL_1, VALUED_1, SEQ_1, SEQ_2, RLVECT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, PRE_TOPC, STRUCT_0, RVSUM_1, FINSEQ_1, FINSEQ_2, FINSEQ_7, SQUARE_1, EUCLID, NORMSP_0, NORMSP_1, REAL_NS1, LOPBAN_1, NFCONT_1, FDIFF_1, NDIFF_1, PDIFF_1, CFDIFF_1, RCOMP_1;
definitions ;
theorems TARSKI, ABSVALUE, XBOOLE_1, XREAL_0, EUCLID, XREAL_1, XXREAL_0, RCOMP_1, RLVECT_1, SEQ_4, COMPLEX1, SEQ_1, SEQ_2, FINSEQ_1, XCMPLX_1, VALUED_1, BINOP_2, FINSEQ_2, FINSEQ_7, RVSUM_1, RELAT_1, FUNCT_1, FUNCT_2, NORMSP_1, LOPBAN_1, PARTFUN1, NFCONT_1, FDIFF_1, NDIFF_1, REAL_NS1, NUMBERS, FUNCT_3, SQUARE_1, CFUNCT_1, CFDIFF_1, PDIFF_1, XCMPLX_0, COMSEQ_1, COMSEQ_2, COMSEQ_3, JGRAPH_1, VECTSP_1, NORMSP_0, CARD_1, ORDINAL1;
schemes FUNCT_2;
registrations RELSET_1, STRUCT_0, ORDINAL1, MEMBERED, NUMBERS, XBOOLE_0, XREAL_0, XXREAL_0, XCMPLX_0, FUNCT_2, REAL_NS1, COMSEQ_3, VALUED_0, VALUED_1, SEQ_4, FDIFF_1, CFDIFF_1, EUCLID, COMSEQ_2, SQUARE_1, RVSUM_1, CFUNCT_1;
constructors HIDDEN, REAL_1, SQUARE_1, RSSPACE3, SEQ_2, BINOP_2, FINSEQ_7, REVROT_1, NFCONT_1, RCOMP_1, FDIFF_1, NDIFF_1, PDIFF_1, CFDIFF_1, COMSEQ_2, COMSEQ_3, RVSUM_1, RELSET_1, BINOP_1, NUMBERS, EXTREAL1;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities LOPBAN_1, EUCLID, COMPLEX1, PDIFF_1, VALUED_1, RVSUM_1, XCMPLX_0, ORDINAL1;
expansions COMPLEX1, PDIFF_1;


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;