PartFunc of COMPLEX,REAL means :Def2:
dom f = dom it &
for z be Complex st z in dom it holds it.z = Re(f/.z);
existence
proof
deffunc f(set) = Re(f/.$1);
defpred P[set] means $1 in dom f;
set X = dom f;
consider F be PartFunc of COMPLEX,REAL such that
A1: for z be Complex holds z in dom F iff P[z] and
A2: for z be Complex st z in dom F holds F.z = f(z) from SEQ_1:sch 3;
take F;
thus dom F = dom f by A1,SUBSET_1:8;
let z be Complex;assume z in dom F;
hence thesis by A2;
end;
uniqueness
proof
deffunc f(set) = Re (f/.$1);
thus for h,g being PartFunc of COMPLEX,REAL st
(dom h=dom f & for z be Complex st z in dom h holds h.z = f(z)) &
(dom g=dom f & for z be Complex st z in dom g holds g.z = f(z))
holds h = g from SEQ_1:sch 4;
end;
end;
definition let f be PartFunc of COMPLEX,COMPLEX; ::: to be removed
func Im f -> PartFunc of COMPLEX,REAL means :Def3:
dom f = dom it & for z be Complex st z in dom it holds it.z=Im (f/.z);
existence
proof
deffunc f(set) = Im (f/.$1);
defpred P[set] means $1 in dom f;
set X = dom f;
consider F be PartFunc of COMPLEX,REAL such that
A1: for z be Complex holds z in dom F iff P[z] and
A2: for z be Complex st z in dom F holds F.z = f(z) from SEQ_1:sch 3;
take F;
thus dom F = dom f by A1,SUBSET_1:8;
let z be Complex;assume z in dom F;
hence thesis by A2;
end;
uniqueness
proof
deffunc f(set) = Im (f/.$1);
thus for h,g being PartFunc of COMPLEX,REAL st
(dom h=dom f & for z be Complex st z in dom h holds h.z = f(z)) &
(dom g=dom f & for z be Complex st z in dom g holds g.z = f(z))
holds h = g from SEQ_1:sch 4;
end;
end;
theorem LM09:
for f be PartFunc of COMPLEX,COMPLEX st f is total
holds dom (Re f) = COMPLEX & dom (Im f) = COMPLEX
proof
let f be PartFunc of COMPLEX,COMPLEX;
assume f is total; then
dom f = COMPLEX by PARTFUN1:def 4;
hence thesis by Def2, Def3;
end;
LM10:
for seq, cseq be Complex_Sequence
st cseq = * (#) seq holds seq is non-zero iff cseq is non-zero
proof
let seq, cseq be Complex_Sequence such that
A1: cseq = (#) seq;
A3: (#) seq is non-zero implies seq is non-zero
proof
assume
A4: (#) seq is non-zero;
now
let n;
( (#) seq).n <> 0c by A4,COMSEQ_1:4; then
* seq.n <> 0c by VALUED_1:6;
hence seq.n <> 0c;
end;
hence thesis by COMSEQ_1:4;
end;
thus seq is non-zero implies cseq is non-zero by COMSEQ_1:41, A1;
assume cseq is non-zero;
hence seq is non-zero by A1, A3;
end;
LM11:
for seq, cseq be Complex_Sequence st cseq = (#) seq holds
seq is convergent_to_0 iff cseq is convergent_to_0
proof
let seq, cseq be Complex_Sequence such that
A1: cseq = (#) seq;
thus seq is convergent_to_0 implies cseq is convergent_to_0
proof
assume
A02: seq is convergent_to_0; then
A2: seq is non-zero & seq is convergent & lim seq = 0 by CFDIFF_1:def 1;
A3: (#) seq is non-zero & (#) seq is convergent
by A02, COMSEQ_1:41, COMSEQ_2:17;
lim ( (#) seq) = * 0 by A2, COMSEQ_2:18
.= 0;
hence cseq is convergent_to_0 by A1, A3, CFDIFF_1:def 1;
end;
assume
A4: cseq is convergent_to_0;
(-) (#) ( (#) seq ) is convergent by A4, A1, COMSEQ_2:17; then
((-) * ) (#) seq is convergent by CFUNCT_1:31; then
A5: seq is convergent by CFUNCT_1:35;
A6: seq is non-zero by A1, A4, LM10;
lim ( (#) seq) = 0 by A1, A4, CFDIFF_1:def 1; then
* lim seq = 0 by A5, COMSEQ_2:18;
hence seq is convergent_to_0 by A5, A6, CFDIFF_1:def 1;
end;
:: Cauchy-Riemann
theorem Th01:
for f be PartFunc of COMPLEX, COMPLEX,
u,v be PartFunc of REAL 2, REAL,
z0 be Complex,
x0, y0 be Real,
xy0 be Element of REAL 2 st
(for x, y be Real st x+y* in dom f holds
<*x,y*> in dom u & u.<*x,y*> = (Re f).(x+y*)) &
(for x,y be Real st x+y* in dom f holds
<*x,y*> in dom v & v.<*x,y*> = (Im f).(x+y*)) &
z0 = x0+y0* & 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
let f be PartFunc of COMPLEX,COMPLEX,
u,v be PartFunc of REAL 2,REAL,
z0 be Complex,
x0,y0 be Real,xy0 be Element of REAL 2 such that
A2: (for x,y be Real st x+y* in dom f holds
<*x,y*> in dom u & u.<*x,y*> = (Re f).(x+y*)) and
A3: (for x,y be Real st x+y* in dom f holds
<*x,y*> in dom v & v.<*x,y*> = (Im f).(x+y*)) and
A4: z0 = x0+y0* & xy0 = <*x0,y0*> & f is_differentiable_in z0;
consider N being Neighbourhood of z0 such that
P1: N c= dom f & ex L be C_LINEAR, R be C_REST st
diff(f,z0) = L/.1r & for z be Complex
st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0) by A4,CFDIFF_1:def 7;
consider L be C_LINEAR, R be C_REST such that
P2: diff(f,z0) = L/.1r & for z be Complex
st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0) by P1;
P2R: dom R = COMPLEX by PARTFUN1:def 4;
P3:
for z be Complex st z in N holds f/.z-f/.z0 = diff(f,z0)*(z-z0)+R/.(z-z0)
proof
let z be Complex;
assume
AS: z in N;
consider a0 be Complex such that
ASS: for w be Complex holds L/.w = a0*w by CFDIFF_1:def 4;
L/.(1r*(z-z0)) = a0*1r*(z-z0) by ASS
.= (L/.1r)*(z-z0) by ASS;
hence thesis by AS, P2;
end;
P4: for x,y be Real st x+y* in N holds
f/.(x+y*)-f/.(x0+y0*)
= diff(f,z0)*((x+y*)-(x0+y0*)) + R/.((x+y*)-(x0+y0*))
by A4, P3;
P5: for x, y be Real holds
diff(f,z0)*((x+y*)-(x0+y0*))
= ((Re diff(f,z0)) * (x-x0)-(Im diff(f,z0))*(y-y0))
+ ((Im diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y-y0))*
proof
let x, y be Real; thus
diff(f,z0)*((x+y*)-(x0+y0*))
= ( Re ( diff(f,z0)) + (Im diff(f,z0)) * )*((x-x0)+(y-y0)*)
by COMPLEX1:29
.= ((Re diff(f,z0)) * (x-x0)-(Im diff(f,z0))*(y-y0))
+ ((Im diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y-y0))*;
end;
P5r:
for x,y be Real holds
Re (diff(f,z0)*((x+y*)-(x0+y0*)))
= (Re diff(f,z0)) * (x-x0)-(Im diff(f,z0))*(y-y0)
proof
let x, y be Real; thus
Re (diff(f,z0)*((x+y*)-(x0+y0*)))
= Re (((Re diff(f,z0)) * (x-x0)-(Im diff(f,z0))*(y-y0))
+ ((Im diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y-y0))* ) by P5
.= (Re diff(f,z0)) * (x-x0)-(Im diff(f,z0))*(y-y0) by COMPLEX1:28;
end;
P5i:
for x,y be Real holds
Im (diff(f,z0)*((x+y*)-(x0+y0*)))
= (Im diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y-y0)
proof
let x, y be Real; thus
Im (diff(f,z0)*((x+y*)-(x0+y0*)))
= Im (((Re diff(f,z0)) * (x-x0)-(Im diff(f,z0))*(y-y0))
+ ((Im diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y-y0))* ) by P5
.= (Im diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y-y0) by COMPLEX1:28;
end;
consider r0 be Real such that
P991: 0*