convergent for Real_Sequence; coherence by SERIES_1:4; end; registration cluster absolutely_summable -> summable for Real_Sequence; coherence; end; registration cluster absolutely_summable for Real_Sequence; existence by Lm2,Th3; end; theorem rseq is convergent implies for p st 0

Complex_Sequence means
:Def1:
it.0 = 1r & for n holds it.(n+1) = it.n * z;
existence
proof
reconsider z9 = z as Element of COMPLEX by XCMPLX_0:def 2;
deffunc f(set,Element of COMPLEX) = In($2*z9,COMPLEX);
consider f being sequence of COMPLEX such that
A1: f.0 = 1r & for n being Nat holds f.(n+1) = f(n,f.n) from NAT_1:sch
12;
take f;
thus f.0 = 1r by A1;
let n;
f.(n+1) = f(n,f.n) by A1;
hence thesis;
end;
uniqueness
proof
let seq1,seq2;
assume that
A2: seq1.0=1r and
A3: for n holds seq1.(n+1)=seq1.n * z and
A4: seq2.0=1r and
A5: for n holds seq2.(n+1)=seq2.n * z;
defpred P[Nat] means seq1.$1 = seq2.$1;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
hence seq1.(k+1) = seq2.k * z by A3
.= seq2.(k+1) by A5;
end;
A7: P[0] by A2,A4;
for n being Nat holds P[n] from NAT_1:sch 2(A7,A6);
hence seq1 = seq2;
end;
end;
definition
let z be Complex, n be Nat;
redefine func z |^ n -> Element of COMPLEX equals
z GeoSeq.n;
coherence by XCMPLX_0:def 2;
compatibility
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
defpred P[Nat] means z|^$1 = z GeoSeq.$1;
let w be Element of COMPLEX;
A1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P[n];
hence z|^(n+1) = z GeoSeq.n*z by NEWTON:6
.= z GeoSeq.(n+1) by Def1;
end;
z|^0 = 1r by COMPLEX1:def 4,NEWTON:4
.= z GeoSeq.0 by Def1;
then
A2: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A2,A1);
then z|^n = z GeoSeq.n;
hence thesis;
end;
end;
theorem
z |^ 0 = 1r by COMPLEX1:def 4,NEWTON:4;
definition
let f be complex-valued Function;
set A = dom f;
deffunc F(object) = Re(f.$1);
func Re f -> Function means
:Def3:
dom it = dom f & for x be object st x in dom it holds it.x = Re(f.x);
existence
proof
ex f being Function st dom f = A &
for x be object st x in A holds f.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let g,h be Function such that
A1: dom g = dom f and
A2: for x be object st x in dom g holds g.x = F(x) and
A3: dom h = dom f and
A4: for x be object st x in dom h holds h.x = F(x);
now
let x be object;
assume
A5: x in dom g;
hence g.x = F(x) by A2
.= h.x by A1,A3,A4,A5;
end;
hence thesis by A1,A3,FUNCT_1:2;
end;
deffunc F(object) = Im(f.$1);
func Im f -> Function means
:Def4:
dom it = dom f & for x be object st x in dom it holds it.x = Im(f.x);
existence
proof
ex f being Function st dom f = A &
for x be object st x in A holds f.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let g,h be Function such that
A6: dom g = dom f and
A7: for x be object st x in dom g holds g.x = F(x) and
A8: dom h = dom f and
A9: for x be object st x in dom h holds h.x = F(x);
now
let x be object;
assume
A10: x in dom g;
hence g.x = F(x) by A7
.= h.x by A6,A8,A9,A10;
end;
hence thesis by A6,A8,FUNCT_1:2;
end;
end;
registration
let f be complex-valued Function;
cluster Re f -> real-valued;
coherence
proof
let x be object;
assume x in dom Re f;
then (Re f).x = Re(f.x) by Def3;
hence thesis;
end;
cluster Im f -> real-valued;
coherence
proof
let x be object;
assume x in dom Im f;
then (Im f).x = Im(f.x) by Def4;
hence thesis;
end;
end;
definition
let X be set, f be PartFunc of X,COMPLEX;
redefine func Re f -> PartFunc of X,REAL;
coherence
proof
A1: dom f c= X by RELAT_1:def 18;
A2: rng Re f c= REAL by VALUED_0:def 3;
dom Re f = dom f by Def3;
hence thesis by A1,A2,RELSET_1:4;
end;
redefine func Im f -> PartFunc of X,REAL;
coherence
proof
A3: dom f c= X by RELAT_1:def 18;
A4: rng Im f c= REAL by VALUED_0:def 3;
dom Im f = dom f by Def4;
hence thesis by A3,A4,RELSET_1:4;
end;
end;
definition
let c be Complex_Sequence;
redefine func Re c -> Real_Sequence means
:Def5:
for n holds it.n = Re(c.n);
coherence
proof
dom Re c = dom c by Def3
.= NAT by FUNCT_2:def 1;
then Re c is total by PARTFUN1:def 2;
hence thesis;
end;
compatibility
proof
let f be Real_Sequence;
A1: dom Re c = dom c by Def3;
A2: dom c = NAT by FUNCT_2:def 1;
A3: dom f = NAT by FUNCT_2:def 1;
thus f = Re c implies
for n holds f.n = Re(c.n) by A1,A2,Def3,ORDINAL1:def 12;
assume
A4: for n holds f.n = Re(c.n);
now
let x be object;
assume
A5: x in dom f;
hence f.x = Re(c.x) by A4
.= (Re c).x by A1,A2,A3,A5,Def3;
end;
hence thesis by A1,A2,A3,FUNCT_1:2;
end;
redefine func Im c -> Real_Sequence means
:Def6:
for n holds it.n = Im(c.n);
coherence
proof
dom Im c = dom c by Def4
.= NAT by FUNCT_2:def 1;
then Im c is total by PARTFUN1:def 2;
hence thesis;
end;
compatibility
proof
let f be Real_Sequence;
A6: dom Im c = dom c by Def4;
A7: dom c = NAT by FUNCT_2:def 1;
A8: dom f = NAT by FUNCT_2:def 1;
thus f = Im c implies
for n holds f.n = Im(c.n) by A6,A7,ORDINAL1:def 12,Def4;
assume
A9: for n holds f.n = Im(c.n);
now
let x be object;
assume
A10: x in dom f;
hence f.x = Im(c.x) by A9
.= (Im c).x by A6,A7,A8,A10,Def4;
end;
hence thesis by A6,A7,A8,FUNCT_1:2;
end;
end;
theorem Th12:
|.z.| <= |.Re z.| + |.Im z.|
proof
z = Re z + (Im z)** by COMPLEX1:13;
then
A1: |.z.| <= |.Re z +0* .| +|.0+(Im z)*.| by COMPLEX1:56;
Re(0+(Im z)*)=0 & Im(0+(Im z)*)=Im z by COMPLEX1:12;
hence thesis by A1,COMPLEX1:51;
end;
theorem Th13:
|.Re z.| <= |.z.| & |.Im z.| <= |.z.|
proof
0 <= (Re z)^2 by XREAL_1:63;
then
A1: 0+(Im z)^2 <= (Re z)^2 + (Im z)^2 by XREAL_1:6;
0 <= (Im z)^2 by XREAL_1:63;
then
A2: sqrt((Im z)^2) <= sqrt((Re z)^2 + (Im z)^2) by A1,SQUARE_1:26;
0 <= (Im z)^2 by XREAL_1:63;
then
A3: 0+(Re z)^2 <= (Im z)^2 + (Re z)^2 by XREAL_1:6;
0 <= (Re z)^2 by XREAL_1:63;
then |.z.| = sqrt ((Re z)^2 + (Im z)^2) & sqrt((Re z)^2) <= sqrt((Re z)^2 +
(Im z )^2) by A3,COMPLEX1:def 12,SQUARE_1:26;
hence thesis by A2,COMPLEX1:72;
end;
theorem Th14:
Re seq1=Re seq2 & Im seq1=Im seq2 implies seq1=seq2
proof
assume that
A1: Re seq1=Re seq2 and
A2: Im seq1=Im seq2;
now
let n be Element of NAT;
A3: Im(seq1.n)=Im seq2.n by A2,Def6
.=Im(seq2.n) by Def6;
Re(seq1.n)=Re seq2.n by A1,Def5
.=Re(seq2.n) by Def5;
hence seq1.n=seq2.n by A3,COMPLEX1:3;
end;
hence thesis;
end;
theorem Th15:
Re seq1 + Re seq2 = Re (seq1+seq2) & Im seq1 + Im seq2 = Im (
seq1+seq2 qua Complex_Sequence)
proof
now
let n be Element of NAT;
thus (Re seq1+Re seq2).n=Re seq1.n+Re seq2.n by SEQ_1:7
.=Re(seq1.n)+Re seq2.n by Def5
.=Re(seq1.n)+Re(seq2.n) by Def5
.=Re(seq1.n+seq2.n) by COMPLEX1:8
.=Re((seq1+seq2).n) by VALUED_1:1
.=Re (seq1+seq2).n by Def5;
end;
hence Re seq1+Re seq2=Re (seq1+seq2);
now
let n be Element of NAT;
thus (Im seq1+Im seq2).n=Im seq1.n+Im seq2.n by SEQ_1:7
.=Im(seq1.n)+Im seq2.n by Def6
.=Im(seq1.n)+Im(seq2.n) by Def6
.=Im(seq1.n+seq2.n) by COMPLEX1:8
.=Im((seq1+seq2).n) by VALUED_1:1
.=Im (seq1+seq2).n by Def6;
end;
hence thesis;
end;
theorem Th16:
-(Re seq) = Re (-seq) & -(Im seq) = Im -seq
proof
now
let n be Element of NAT;
thus (-Re seq).n= -(Re seq.n) by SEQ_1:10
.=-Re(seq.n) by Def5
.= Re(-(seq.n)) by COMPLEX1:17
.= Re((-seq).n) by VALUED_1:8
.=Re (-seq).n by Def5;
end;
hence -Re seq=Re (-seq);
now
let n be Element of NAT;
thus (-Im seq).n=-Im seq.n by SEQ_1:10
.=-Im(seq.n) by Def6
.= Im(-(seq.n)) by COMPLEX1:17
.= Im((-seq).n) by VALUED_1:8
.=(Im -seq).n by Def6;
end;
hence thesis;
end;
theorem Th17:
r*Re(z)=Re(r*z) & r*Im(z)=Im(r*z)
proof
reconsider r9 = r as Element of COMPLEX by XCMPLX_0:def 2;
r = r +0*;
then
A1: Re r = r & Im r = 0 by COMPLEX1:12;
r*z = Re r9 * Re z - Im r9 * Im z + (Re r9 * Im z + Re z * Im r9)* by
COMPLEX1:82
.= r * Re z+(r * Im z)* by A1;
hence thesis by COMPLEX1:12;
end;
theorem Th18:
Re seq1-Re seq2=Re (seq1-seq2) & Im seq1-Im seq2=Im(seq1-seq2)
proof
now
let n be Element of NAT;
thus (Re seq1-Re seq2).n = Re seq1.n+(-Re seq2).n by SEQ_1:7
.=Re seq1.n+(Re -seq2).n by Th16
.=(Re seq1+Re -seq2).n by SEQ_1:7
.=Re (seq1-seq2).n by Th15;
end;
hence Re seq1-Re seq2=Re (seq1-seq2);
now
let n be Element of NAT;
thus (Im seq1-Im seq2).n = Im seq1.n+(-Im seq2).n by SEQ_1:7
.=Im seq1.n+Im (-seq2).n by Th16
.=(Im seq1+Im -seq2).n by SEQ_1:7
.=Im(seq1-seq2).n by Th15;
end;
hence thesis;
end;
theorem
r(#)Re seq = Re (r (#) seq) & r(#)Im seq = Im (r (#) seq)
proof
now
let n be Element of NAT;
thus (r(#)Re seq).n= r*(Re seq.n) by SEQ_1:9
.=r*Re(seq.n) by Def5
.=Re(r*(seq.n)) by Th17
.=Re((r (#) seq).n) by VALUED_1:6
.=Re (r (#) seq).n by Def5;
end;
hence r(#)Re seq=Re (r (#) seq);
now
let n be Element of NAT;
thus (r(#)Im seq).n= r*(Im seq.n) by SEQ_1:9
.=r*Im(seq.n) by Def6
.=Im(r*(seq.n)) by Th17
.=Im((r(#) seq).n) by VALUED_1:6
.=Im(r(#)seq).n by Def6;
end;
hence thesis;
end;
theorem
Re (z (#) seq) = Re z (#) Re seq - Im z (#) Im seq & Im (z (#) seq) =
Re z (#) Im seq + Im z (#) Re seq
proof
now
let n be Element of NAT;
thus Re (z (#) seq).n=Re((z (#) seq).n) by Def5
.= Re((z * seq.n )) by VALUED_1:6
.= Re(Re(z) * Re(seq.n) - Im(z) * Im(seq.n)+ (Re(z) * Im(seq.n) + Re(
seq.n) * Im(z))*) by COMPLEX1:82
.= Re(z) * Re(seq.n) - Im(z) * Im(seq.n) by COMPLEX1:12
.= Re(z) *( Re seq.n) - Im(z) * Im(seq.n) by Def5
.= Re(z) *( Re seq.n) - Im(z) *( Im seq.n) by Def6
.= (Re(z) (#) Re seq).n - Im(z) *( Im seq.n) by SEQ_1:9
.= (Re(z) (#) Re seq).n - (Im(z) (#) Im seq).n by SEQ_1:9
.= (Re(z) (#) Re seq).n + (- (Im(z) (#) Im seq).n)
.= (Re(z) (#) Re seq).n + (- Im(z) (#) Im seq).n by SEQ_1:10
.= (Re(z) (#) Re seq - Im(z) (#) Im seq).n by SEQ_1:7;
end;
hence Re (z (#) seq)=Re(z)(#)Re seq-Im(z)(#)Im seq;
now
let n be Element of NAT;
thus Im(z(#)seq).n =Im((z (#) seq).n) by Def6
.=Im((z * seq.n )) by VALUED_1:6
.=Im(Re(z) * Re(seq.n) - Im(z) * Im(seq.n)+ (Re(z) * Im(seq.n) + Re(
seq.n) * Im(z))*) by COMPLEX1:82
.= Re(z) * Im(seq.n) + Re(seq.n) * Im(z) by COMPLEX1:12
.= Re(z) * Im(seq.n) + Im(z) * Re seq.n by Def5
.= Re(z) * Im seq.n + Im(z) *(Re seq.n) by Def6
.= (Re(z) (#) Im seq).n + Im(z) *(Re seq.n) by SEQ_1:9
.= (Re(z) (#) Im seq).n + (Im(z) (#) Re seq).n by SEQ_1:9
.= (Re(z) (#) Im seq + Im(z) (#) Re seq).n by SEQ_1:7;
end;
hence thesis;
end;
theorem
Re (seq1 (#) seq2) = Re seq1(#)Re seq2-Im seq1(#)Im seq2 & Im (seq1
(#) seq2) = Re seq1(#)Im seq2+Im seq1(#)Re seq2
proof
now
let n be Element of NAT;
thus Re (seq1 (#) seq2).n=Re((seq1 (#) seq2).n) by Def5
.=Re((seq1.n * seq2.n )) by VALUED_1:5
.=Re(Re(seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n)+ (Re(seq1.n) *
Im(seq2.n) + Re(seq2.n) * Im(seq1.n))*) by COMPLEX1:82
.= Re(seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n) by COMPLEX1:12
.= (Re seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n) by Def5
.= (Re seq1.n) *( Re seq2.n) - Im(seq1.n) * Im(seq2.n) by Def5
.= (Re seq1.n) *( Re seq2.n) - Im(seq1.n) *( Im seq2.n) by Def6
.= (Re seq1.n) *( Re seq2.n) - (Im seq1.n)*( Im seq2.n) by Def6
.= (Re seq1 (#) Re seq2).n - (Im seq1.n) *( Im seq2.n) by SEQ_1:8
.= (Re seq1 (#) Re seq2).n - (Im seq1 (#) Im seq2).n by SEQ_1:8
.= (Re seq1 (#)Re seq2).n + (- (Im seq1 (#) Im seq2).n)
.= (Re seq1 (#) Re seq2).n + (- Im seq1 (#) Im seq2).n by SEQ_1:10
.= (Re seq1 (#) Re seq2 - Im seq1 (#) Im seq2).n by SEQ_1:7;
end;
hence Re (seq1 (#) seq2)=Re seq1(#)Re seq2-Im seq1(#)Im seq2;
now
let n be Element of NAT;
thus Im (seq1 (#) seq2).n =Im((seq1 (#) seq2).n) by Def6
.=Im((seq1.n * seq2.n )) by VALUED_1:5
.=Im(Re(seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n)+ (Re(seq1.n) *
Im(seq2.n) + Re(seq2.n) * Im(seq1.n))*) by COMPLEX1:82
.= Re(seq1.n) * Im(seq2.n) + Re(seq2.n) * Im(seq1.n) by COMPLEX1:12
.= Re(seq1.n) * Im(seq2.n) + Im(seq1.n) * Re seq2.n by Def5
.= Re seq1.n * Im(seq2.n) + Im(seq1.n) * Re seq2.n by Def5
.= Re seq1.n * Im seq2.n + Im(seq1.n) * Re seq2.n by Def6
.= (Re seq1.n * Im seq2.n) + (Im seq1.n * Re seq2.n) by Def6
.= (Re seq1 (#) Im seq2).n + Im seq1.n *( Re seq2.n) by SEQ_1:8
.= (Re seq1 (#) Im seq2).n + (Im seq1 (#) Re seq2).n by SEQ_1:8
.= (Re seq1 (#) Im seq2 + Im seq1 (#) Re seq2).n by SEQ_1:7;
end;
hence thesis;
end;
definition
let Nseq be increasing sequence of NAT, seq be Complex_Sequence;
redefine func seq * Nseq -> Complex_Sequence;
coherence
proof
dom (seq*Nseq)=NAT by FUNCT_2:def 1;
hence thesis;
end;
end;
theorem Th22:
Re (seq*Nseq)=(Re seq)*Nseq & Im (seq*Nseq)=(Im seq)*Nseq
proof
now
let n be Element of NAT;
thus (Re (seq*Nseq)).n =Re((seq*Nseq).n) by Def5
.=Re(seq.(Nseq.n)) by FUNCT_2:15
.=Re seq.(Nseq.n) by Def5
.=(Re seq*Nseq).n by FUNCT_2:15;
end;
hence Re (seq*Nseq)=Re seq*Nseq;
now
let n be Element of NAT;
thus Im (seq*Nseq).n =Im((seq*Nseq).n) by Def6
.=Im(seq.(Nseq.n)) by FUNCT_2:15
.=Im seq.(Nseq.n) by Def6
.=(Im seq*Nseq).n by FUNCT_2:15;
end;
hence thesis;
end;
theorem Th23:
(Re seq)^\k =Re (seq^\k) & (Im seq)^\k =Im (seq^\k)
proof
now
let n be Element of NAT;
thus (Re seq^\k).n =Re seq.(n+k) by NAT_1:def 3
.=Re(seq.(n+k)) by Def5
.=Re((seq^\k).n) by NAT_1:def 3
.=Re ((seq)^\k).n by Def5;
thus (Im seq^\k).n =Im seq.(n+k) by NAT_1:def 3
.=Im(seq.(n+k)) by Def6
.=Im((seq^\k).n) by NAT_1:def 3
.=Im ((seq)^\k).n by Def6;
end;
hence thesis;
end;
definition
let s be Complex_Sequence;
redefine func Partial_Sums s -> Complex_Sequence;
coherence
proof
A1: dom Partial_Sums s = NAT by PARTFUN1:def 2;
rng Partial_Sums s c= COMPLEX by VALUED_0:def 1;
then Partial_Sums s is PartFunc of NAT, COMPLEX by A1,RELSET_1:4;
hence Partial_Sums s is Complex_Sequence;
end;
end;
definition
let seq be Complex_Sequence;
func Sum seq -> Element of COMPLEX equals
lim Partial_Sums seq;
coherence by XCMPLX_0:def 2;
end;
theorem Th24:
(for n holds seq.n = 0c) implies for m holds (Partial_Sums seq). m = 0c
proof
defpred P[Nat] means seq.$1 = (Partial_Sums seq).$1;
assume
A1: for n holds seq.n = 0c;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
thus seq.(k+1) = 0c + seq.(k+1)
.= (Partial_Sums seq).k + seq.(k+1) by A1,A3
.= (Partial_Sums seq).(k+1) by SERIES_1:def 1;
end;
let m;
A4: P[0] by SERIES_1:def 1;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
then seq = Partial_Sums seq;
hence thesis by A1;
end;
theorem Th25:
(for n holds seq.n = 0c) implies for m holds (Partial_Sums |.seq .|).m = 0
proof
defpred P[Nat] means |.seq.|.$1 = (Partial_Sums |.seq.|).$1;
assume
A1: for n holds seq.n = 0c;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
thus |.seq.|.(k+1) = |.0c.| + |.seq.|.(k+1) by COMPLEX1:44
.= |.seq.k.| + |.seq.|.(k+1) by A1
.= (Partial_Sums |.seq.|).k + |.seq.|.(k+1) by A3,VALUED_1:18
.= (Partial_Sums |.seq.|).(k+1) by SERIES_1:def 1;
end;
let m;
A4: P[0] by SERIES_1:def 1;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence (Partial_Sums |.seq.|).m = |.seq.|.m .= |.seq.m.| by VALUED_1:18
.= 0 by A1,COMPLEX1:44;
end;
theorem Th26:
Partial_Sums Re seq = Re (Partial_Sums seq) & Partial_Sums Im
seq = Im (Partial_Sums seq)
proof
defpred P[Nat] means
Partial_Sums(Re seq).$1 = Re Partial_Sums(
seq).$1;
defpred R[Nat] means
Partial_Sums(Im seq).$1 = Im Partial_Sums(seq).$1;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then Partial_Sums(Re seq).(k+1) =Re Partial_Sums(seq).k + Re seq.(k+1) by
SERIES_1:def 1
.=Re Partial_Sums(seq).k +Re(seq.(k+1)) by Def5
.=Re(Partial_Sums(seq).k) +Re(seq.(k+1)) by Def5
.=Re(Partial_Sums(seq).k + seq.(k+1)) by COMPLEX1:8
.=Re(Partial_Sums(seq).(k+1)) by SERIES_1:def 1
.=Re Partial_Sums(seq).(k+1) by Def5;
hence thesis;
end;
A2: for k be Nat st R[k] holds R[k+1]
proof
let k be Nat;
assume R[k];
then
Partial_Sums(Im seq).(k+1) = Im Partial_Sums(seq).k + Im seq.(k+1) by
SERIES_1:def 1
.=Im Partial_Sums(seq).k +Im(seq.(k+1)) by Def6
.=Im(Partial_Sums(seq).k) +Im(seq.(k+1)) by Def6
.=Im(Partial_Sums(seq).k + seq.(k+1)) by COMPLEX1:8
.=Im(Partial_Sums(seq).(k+1)) by SERIES_1:def 1
.=Im Partial_Sums(seq).(k+1) by Def6;
hence thesis;
end;
Partial_Sums(Im seq).0 = Im seq.0 by SERIES_1:def 1
.= Im(seq.0) by Def6
.= Im(Partial_Sums(seq).0) by SERIES_1:def 1
.= Im Partial_Sums(seq).0 by Def6;
then
A3: R[0];
A4: for n being Nat holds R[n] from NAT_1:sch 2(A3,A2);
Partial_Sums(Re seq).0 = Re seq.0 by SERIES_1:def 1
.= Re(seq.0) by Def5
.= Re(Partial_Sums(seq).0) by SERIES_1:def 1
.= Re Partial_Sums(seq).0 by Def5;
then
A5: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A5,A1);
hence thesis by A4;
end;
theorem Th27:
Partial_Sums(seq1)+Partial_Sums(seq2) = Partial_Sums(seq1+seq2)
by SERIES_1:5;
theorem Th28:
Partial_Sums(seq1)-Partial_Sums(seq2) = Partial_Sums(seq1-seq2)
proof
A1: Im(Partial_Sums(seq1)-Partial_Sums(seq2)) =Im Partial_Sums(seq1)-Im
Partial_Sums(seq2) by Th18
.=Partial_Sums Im seq1-Im Partial_Sums(seq2) by Th26
.=Partial_Sums Im seq1-Partial_Sums Im seq2 by Th26
.=Partial_Sums(Im seq1-Im seq2) by SERIES_1:6
.=Partial_Sums(Im (seq1-seq2)) by Th18
.=Im Partial_Sums(seq1-seq2) by Th26;
Re (Partial_Sums(seq1)-Partial_Sums(seq2)) =Re Partial_Sums(seq1)-Re
Partial_Sums(seq2) by Th18
.=Partial_Sums Re seq1-Re Partial_Sums(seq2) by Th26
.=Partial_Sums Re seq1-Partial_Sums Re seq2 by Th26
.=Partial_Sums(Re seq1-Re seq2) by SERIES_1:6
.=Partial_Sums(Re (seq1-seq2)) by Th18
.=Re Partial_Sums(seq1-seq2) by Th26;
hence thesis by A1,Th14;
end;
theorem Th29:
for z being Complex holds Partial_Sums(z (#) seq) = z (#)
Partial_Sums(seq)
proof
let z be Complex;
defpred P[Nat] means Partial_Sums(z (#) seq).$1= (z (#)
Partial_Sums(seq)).$1;
A1: now
let n be Nat;
assume
A2: P[n];
Partial_Sums(z (#) seq).(n+1) =Partial_Sums(z (#) seq).n + (z (#) seq)
.(n+1) by SERIES_1:def 1
.=(z * Partial_Sums(seq).n )+ (z (#) seq).(n+1) by A2,VALUED_1:6
.=(z * Partial_Sums(seq).n )+ (z * seq.(n+1)) by VALUED_1:6
.= z * ( Partial_Sums(seq).n + seq.(n+1))
.= z * ( Partial_Sums(seq).(n+1)) by SERIES_1:def 1
.= (z (#) Partial_Sums(seq)).(n+1) by VALUED_1:6;
hence P[n+1];
end;
Partial_Sums(z(#)seq).0=(z (#) seq).0 by SERIES_1:def 1
.=z * seq.0 by VALUED_1:6
.=z * Partial_Sums(seq).0 by SERIES_1:def 1
.=(z (#) Partial_Sums(seq)).0 by VALUED_1:6;
then
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
|.Partial_Sums(seq).k.| <= (Partial_Sums |.seq.|).k
proof
defpred P[Nat] means
|. Partial_Sums(seq).$1 .| <= Partial_Sums(|.seq.|).$1;
A1: now
let k;
assume P[k];
then
A2: |. Partial_Sums(seq).k.| + |.(seq).(k+1).| <= Partial_Sums(|.seq.| ).k
+ |.(seq).(k+1).| by XREAL_1:6;
|. Partial_Sums(seq).(k+1) .| =|. Partial_Sums(seq).k + (seq).(k+1) .|
& |. Partial_Sums(seq).k + (seq).(k+1) .| <= |. Partial_Sums(seq).k.| + |. (seq
).(k+ 1) .| by COMPLEX1:56,SERIES_1:def 1;
then
|. Partial_Sums(seq).(k+1) .| <= Partial_Sums(|.seq.|).k + |.seq.(k+1)
.| by A2,XXREAL_0:2;
then
|. Partial_Sums(seq).(k+1) .| <= Partial_Sums(|.seq.|).k+|.seq.|.(k+1)
by VALUED_1:18;
hence P[k+1] by SERIES_1:def 1;
end;
Partial_Sums(|.seq.|).0 = (|.seq.|).0 by SERIES_1:def 1
.= |. seq.0 .| by VALUED_1:18;
then
A3: P[0] by SERIES_1:def 1;
for k being Nat holds P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th31:
|.Partial_Sums(seq).m- Partial_Sums(seq).n.| <= |.
Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n.|
proof
A1: for n,k be Nat holds 0 <= Partial_Sums(|.seq.|).(n+k)-
Partial_Sums(|.seq.|).n
proof
let n;
defpred P[Nat] means 0 <= Partial_Sums(|.seq.|).(n+$1)-
Partial_Sums(|.seq.|).n;
A2: now
let k;
A3: Partial_Sums(|.seq.|).(n+(k+1))- Partial_Sums(|.seq.|).n =
Partial_Sums(|.seq.|).(n+k)+|.seq.|.(n+k+1) - Partial_Sums(|.seq.|).n by
SERIES_1:def 1
.=Partial_Sums(|.seq.|).(n+k)+|.seq.(n+k+1).| - Partial_Sums(|.seq.|
).n by VALUED_1:18
.=Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n +|.seq.(n+k+1
).|;
A4: 0 <= |.seq.(n+k+1).| by COMPLEX1:46;
assume P[k];
hence P[k+1] by A3,A4;
end;
A5: P[0];
thus for k be Nat holds P[k] from NAT_1:sch 2(A5,A2);
end;
A6: for n,k be Nat holds |. Partial_Sums(|.seq.|).(n+k)-
Partial_Sums(|.seq.|).n.|
= Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n by A1,ABSVALUE:def 1;
A7:
for n,m st n <= m holds |.Partial_Sums(seq).m- Partial_Sums(seq).n
.| <= |. Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n.|
proof
let n,m be Nat;
assume n <= m;
then consider k be Nat such that
A8: m=n+k by NAT_1:10;
A9: for k be Nat holds |.Partial_Sums(seq).(n+k)- Partial_Sums
(seq).n.| <= |. Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n.|
proof
defpred P[Nat] means |.Partial_Sums(seq).(n+$1)- Partial_Sums
(seq).n.| <= |. Partial_Sums(|.seq.|).(n+$1)- Partial_Sums(|.seq.|).n.|;
A10: now
let k be Nat;
assume P[k];
then
A11: |.Partial_Sums(seq).(n+k)- Partial_Sums(seq).n+seq.(n+k+1).| <=
|. Partial_Sums(seq).(n+k)- Partial_Sums(seq).n.| +|.seq.(n+k+1).| & |.
Partial_Sums(seq).(n+k)- Partial_Sums(seq).n.| +|.seq.(n+k+1).| <= |.
Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n .| +|.seq.(n+k+1).| by
COMPLEX1:56,XREAL_1:6;
A12: |.Partial_Sums(seq).(n+(k+1))- Partial_Sums(seq).n .| =|.(
Partial_Sums(seq).(n+k)+seq.(n+k+1))- Partial_Sums(seq).n.|
by SERIES_1:def 1
.=|.Partial_Sums(seq).(n+k)- Partial_Sums(seq).n+seq.(n+k+1).|;
|. Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n .| +|.
seq.(n+k+1).| =Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n +|.seq.(n+k
+1).| by A6
.=Partial_Sums(|.seq.|).(n+k)+|.seq.(n+k+1).| - Partial_Sums(|.seq
.|).n
.=Partial_Sums(|.seq.|).(n+k)+|.seq.|.(n+k+1) - Partial_Sums(|.seq
.|).n by VALUED_1:18
.=Partial_Sums(|.seq.|).(n+(k+1))- Partial_Sums(|.seq.|).n by
SERIES_1:def 1
.=|. Partial_Sums(|.seq.|).(n+(k+1))- Partial_Sums(|.seq.|).n .|
by A6;
hence P[k+1] by A12,A11,XXREAL_0:2;
end;
A13: P[0];
thus for k be Nat holds P[k] from NAT_1:sch 2(A13,A10 );
end;
thus thesis by A9,A8;
end;
for n, m holds |.Partial_Sums(seq).m- Partial_Sums(seq).n.| <= |.
Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n .|
proof
let n,m;
m <= n implies |.Partial_Sums(seq).m- Partial_Sums(seq).n.| <= |.
Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n .|
proof
assume m <= n;
then
A14: |.Partial_Sums(seq).n- Partial_Sums(seq).m.| <= |. Partial_Sums(
|.seq.|).n- Partial_Sums(|.seq.|).m .| by A7;
|. Partial_Sums(|.seq.|).n- Partial_Sums(|.seq.|).m .| =|.-(
Partial_Sums(|.seq.|).n- Partial_Sums(|.seq.|).m) .| by COMPLEX1:52
.=|. Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n .|;
hence thesis by A14,COMPLEX1:60;
end;
hence thesis by A7;
end;
hence thesis;
end;
theorem Th32:
Partial_Sums(Re seq)^\k =Re (Partial_Sums(seq)^\k) &
Partial_Sums(Im seq)^\k =Im (Partial_Sums(seq)^\k)
proof
now
let n be Element of NAT;
thus (Partial_Sums(Re seq)^\k).n =Partial_Sums(Re seq).(n+k) by NAT_1:def 3
.=Re Partial_Sums(seq).(n+k) by Th26
.=Re(Partial_Sums(seq).(n+k)) by Def5
.=Re((Partial_Sums(seq)^\k).n) by NAT_1:def 3
.=(Re (Partial_Sums(seq)^\k)).n by Def5;
thus (Partial_Sums(Im seq)^\k).n =Partial_Sums(Im seq).(n+k) by NAT_1:def 3
.=Im Partial_Sums(seq).(n+k) by Th26
.=Im(Partial_Sums(seq).(n+k)) by Def6
.=Im((Partial_Sums(seq)^\k).n) by NAT_1:def 3
.=Im (Partial_Sums(seq)^\k).n by Def6;
end;
hence thesis;
end;
theorem
(for n holds seq1.n=seq.0) implies Partial_Sums(seq^\1) = (
Partial_Sums(seq)^\1) - seq1
proof
assume
A1: for n holds seq1.n=seq.0;
A2: now
let n;
thus Re seq1.n=Re(seq1.n) by Def5
.=Re(seq.0) by A1
.=Re seq.0 by Def5;
thus Im seq1.n=Im(seq1.n) by Def6
.=Im(seq.0) by A1
.=Im seq.0 by Def6;
end;
A3: Im Partial_Sums(seq^\1)=Partial_Sums(Im (seq^\1)) by Th26
.=Partial_Sums(Im seq^\1) by Th23
.= (Partial_Sums(Im seq)^\1) - Im seq1 by A2,SERIES_1:11
.=Im (Partial_Sums(seq)^\1)-Im seq1 by Th32
.=Im (Partial_Sums(seq)^\1-seq1) by Th18;
Re Partial_Sums(seq^\1)=Partial_Sums(Re (seq^\1)) by Th26
.=Partial_Sums(Re seq^\1) by Th23
.= (Partial_Sums(Re seq)^\1) - Re seq1 by A2,SERIES_1:11
.=Re (Partial_Sums(seq)^\1)-Re seq1 by Th32
.=Re (Partial_Sums(seq)^\1-seq1) by Th18;
hence thesis by A3,Th14;
end;
theorem Th34:
Partial_Sums |.seq.| is non-decreasing
proof
for n holds 0 <= |.seq.|.n by Lm3;
hence thesis by SERIES_1:16;
end;
registration
let seq be Complex_Sequence;
cluster Partial_Sums |.seq.| -> non-decreasing for Real_Sequence;
coherence by Th34;
end;
theorem
(for n st n <= m holds seq1.n = seq2.n) implies Partial_Sums(seq1).m =
Partial_Sums(seq2).m
proof
defpred P[Nat] means $1 <= m implies Partial_Sums(seq1).$1=
Partial_Sums(seq2).$1;
assume
A1: for n st n <= m holds seq1.n = seq2.n;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
assume
A4: k+1 <= m;
k < k+1 by XREAL_1:29;
hence Partial_Sums(seq1).(k+1) =Partial_Sums(seq2).k+seq1.(k+1) by A3,A4,
SERIES_1:def 1,XXREAL_0:2
.=Partial_Sums(seq2).k+seq2.(k+1) by A1,A4
.=Partial_Sums(seq2).(k+1) by SERIES_1:def 1;
end;
A5: P[0]
proof
assume 0 <= m;
thus Partial_Sums(seq1).0=seq1.0 by SERIES_1:def 1
.=seq2.0 by A1
.=Partial_Sums(seq2).0 by SERIES_1:def 1;
end;
for k holds P[k] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem Th36:
1r <> z implies for n holds Partial_Sums(z GeoSeq).n = (1r - z
|^ (n+1))/(1r-z)
proof
now
let z;
defpred P[Nat] means
Partial_Sums(z GeoSeq).$1 = (1r - z |^ ($1+1))/(1r-z);
assume 1r <> z;
then
A1: 1r-z <>0c;
A2: for n st P[n] holds P[n+1]
proof
let n;
assume P[n];
hence
Partial_Sums(z GeoSeq).(n+1) = (1r - z |^ (n+1))/(1r-z)+ z |^ (n+1)
* 1r by COMPLEX1:def 4,SERIES_1:def 1
.= (1r - z |^ (n+1))/(1r-z)+ z |^ (n+1) * ((1r-z)/(1r-z)) by A1,
COMPLEX1:def 4,XCMPLX_1:60
.= (1r - z |^ (n+1))/(1r-z)+ (z |^ (n+1) * (1r-z))/(1r-z) by
XCMPLX_1:74
.= (1r - z |^ (n+1) + (z |^ (n+1) -z |^(n+1) * z ))/(1r-z) by
COMPLEX1:def 4,XCMPLX_1:62
.= (1r - z |^(n+1) * z )/(1r-z)
.= (1r - z |^ ((n+1) +1) )/(1r-z) by NEWTON:6;
end;
Partial_Sums(z GeoSeq).0 =(z GeoSeq).0 by SERIES_1:def 1
.=1r by Def1
.=(1r -1 * z )/(1r-z) by A1,COMPLEX1:def 4,XCMPLX_1:60
.=(1r-z |^ (0+1) )/(1r-z);
then
A3: P[0];
thus for n holds P[n] from NAT_1:sch 2(A3,A2);
end;
hence thesis;
end;
theorem Th37:
z <> 1r & (for n holds seq.(n+1) = z * seq.n) implies for n
holds Partial_Sums(seq).n = seq.0 * ((1r - z |^ (n+1))/(1r-z))
proof
assume that
A1: z <> 1r and
A2: for n holds seq.(n+1) = z * seq.n;
defpred P[Nat] means seq.$1=seq.0 * (z GeoSeq).$1;
A3: now
let n be Nat;
assume P[n];
then seq.(n+1)=z * (seq.0 * (z GeoSeq).n) by A2
.=seq.0 * (z * (z GeoSeq).n)
.=seq.0 * (z GeoSeq).(n+1) by Def1;
hence P[n+1];
end;
let n;
seq.0 = seq.0 * 1r by COMPLEX1:def 4
.= seq.0 * (z GeoSeq).0 by Def1;
then
A4: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A4,A3);
then for n being Element of NAT holds P[n];
then Partial_Sums(seq)=Partial_Sums(seq.0 (#) (z GeoSeq)) by VALUED_1:7
.=seq.0 (#) Partial_Sums(z GeoSeq) by Th29;
hence Partial_Sums(seq).n=seq.0 * Partial_Sums(z GeoSeq).n by VALUED_1:6
.=seq.0 * ( (1r - z |^ (n+1))/(1r -z) ) by A1,Th36;
end;
begin :: Convergence of Complex Sequences
theorem Th38:
for a, b being Real_Sequence, c being Complex_Sequence st (for n
holds Re (c.n) = a.n & Im (c.n) = b.n) holds a is convergent & b is convergent
iff c is convergent
proof
let a, b be Real_Sequence, c be Complex_Sequence such that
A1: for n holds Re(c.n) = a.n & Im(c.n) = b.n;
thus a is convergent & b is convergent implies c is convergent
proof
assume that
A2: a is convergent and
A3: b is convergent;
consider a1 being Real such that
A4: for p being Real st 0*

* as Element of COMPLEX by XCMPLX_0:def 2;
take g;
for p st 0*

*0;
consider n such that
A21: for m st n <= m holds |.c.m-z.| < p by A16,A20;
take n;
let m;
assume n <= m;
then
A22: |.c.m-z.| < p by A21;
A23: Im(c.m-z)=Im(c.m)-Im(z) by COMPLEX1:19;
Im(c.m) =b.m by A1;
then |.b.m-Im(z) .| <= |.c.m-z.| by A23,Th13;
hence thesis by A22,XXREAL_0:2;
end;
theorem Th39:
for a, b being convergent Real_Sequence, c being
Complex_Sequence st (for n holds Re (c.n) = a.n & Im (c.n) = b.n) holds c is
convergent & lim(c)= lim(a) + lim(b)*
proof
let a, b be convergent Real_Sequence, c be Complex_Sequence;
reconsider g=lim(a)+lim(b)* as Element of COMPLEX by XCMPLX_0:def 2;
assume
A1: for n holds Re(c.n) = a.n & Im(c.n) = b.n;
hence
A2: c is convergent by Th38;
for p being Real st 0*

*0;
consider n such that
A4: for m st n <= m holds |.c.m-lim(c).| < p by A3,COMSEQ_2:def 6;
take n;
let m;
assume n <= m;
then
A5: |.c.m-lim(c).| < p by A4;
Im(c.m) =b.m & Im(c.m-lim(c))=Im(c.m)-Im(lim(c)) by A1,COMPLEX1:19;
then |.b.m-Im(lim(c)) .| <= |.c.m-lim(c).| by Th13;
hence thesis by A5,XXREAL_0:2;
end;
A6: for p being Real st 0*

* convergent for Real_Sequence;
coherence by Th41;
cluster Im c -> convergent for Real_Sequence;
coherence by Th41;
end;
theorem Th42:
for c being Complex_Sequence st Re c is convergent & Im c is
convergent holds c is convergent & Re(lim(c))=lim(Re c) & Im (lim(c))=lim(Im c)
proof
let c be Complex_Sequence;
assume
A1: Re c is convergent & Im c is convergent;
A2: ( for n holds Re c.n=Re(c.n))& for n holds Im c.n=Im(c.n) by Def5,Def6;
then lim(c) = lim(Re c)+(lim(Im c))* by A1,Th39;
hence thesis by A1,A2,Th39,COMPLEX1:12;
end;
theorem Th43:
(0 < |.z.| & |.z.| < 1 & seq.0 = z & for n holds seq.(n+1) = seq
.n * z) implies seq is convergent & lim(seq)=0c
proof
assume that
A1: 0 < |.z.| and
A2: |.z.| < 1;
deffunc g(Nat) = |.z.| to_power ($1+1);
consider rseq1 such that
A3: for n holds rseq1.n=g(n) from SEQ_1:sch 1;
assume that
A4: seq.0 = z and
A5: for n holds seq.(n+1) = seq.n * z;
A6: for n holds |.seq.n.| = |.z.| to_power (n+1)
proof
defpred P[Nat] means |. seq.$1 .|= |.z.| to_power ($1+1);
A7: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A8: P[k];
|.seq.(k+1).| = |.seq.k * z.| by A5
.= |.z.| to_power (k+1) * |.z.| by A8,COMPLEX1:65
.= |.z.| to_power (k+1) * |.z.| to_power 1 by POWER:25
.= |.z.| to_power ((k+1)+1) by A1,POWER:27;
hence thesis;
end;
A9: P[0] by A4,POWER:25;
for n holds P[n] from NAT_1:sch 2(A9,A7);
hence thesis;
end;
A10: now
let n;
abs(Re seq).n = |.Re seq.n.| by SEQ_1:12;
then
A11: abs(Re seq).n = |.Re(seq.n).| by Def5;
|.Re(seq.n).| <= |.seq.n.| & |.seq.n.| = |.z.| to_power (n+1) by A6,Th13;
hence abs(Re seq).n <= rseq1.n by A3,A11;
end;
A12: now
let n;
A13: |.seq.n.| = |.z.| to_power (n+1) by A6;
abs(Im seq).n = |.Im seq.n.| & |.Im(seq.n).| <= |.seq.n.| by Th13,
SEQ_1:12;
then abs(Im seq).n <= |.z.| to_power (n+1) by A13,Def6;
hence abs(Im seq).n <= rseq1.n by A3;
end;
C.0=0;
then
A14: lim(C)=0 by SEQ_4:25;
A15: rseq1 is convergent & lim(rseq1)=0 by A1,A2,A3,SERIES_1:1;
now
let n;
abs(Re seq).n=|.Re seq.n.| by SEQ_1:12;
then 0 <= abs(Re seq).n by COMPLEX1:46;
hence C.n <= abs(Re seq).n;
end;
then
A16: abs(Re seq) is convergent & lim(abs(Re seq))=0 by A14,A15,A10,SEQ_2:19,20;
then
A17: Re seq is convergent by SEQ_4:15;
now
let n;
abs(Im seq).n=|.Im seq.n.| by SEQ_1:12;
then 0 <= abs(Im seq).n by COMPLEX1:46;
hence C.n <= abs(Im seq).n;
end;
then
A18: abs(Im seq) is convergent & lim(abs(Im seq))=0 by A14,A15,A12,SEQ_2:19,20;
then
A19: Im seq is convergent by SEQ_4:15;
lim(Im seq)=0 by A18,SEQ_4:15;
then
A20: Im lim(seq)=0 by A17,A19,Th42;
lim(Re seq)=0 by A16,SEQ_4:15;
then Re lim(seq)=0 by A17,A19,Th42;
hence thesis by A17,A19,A20,Lm1,Th42,COMPLEX1:13;
end;
theorem Th44:
|.z.| < 1 & (for n holds seq.n=z |^ (n+1)) implies seq is
convergent & lim(seq)=0c
proof
assume that
A1: |.z.| <1 and
A2: for n holds seq.n=z |^ (n+1);
A3: now
let n;
thus seq.(n+1) = z |^ ((n+1)+1) by A2
.= z |^ (n+1) * z by NEWTON:6
.= seq.n * z by A2;
end;
A4: now
assume |.z.| = 0;
then
A5: z =0c by COMPLEX1:45;
A6: now
let n;
thus seq.n = 0c |^ (n+1) by A2,A5
.=(0c GeoSeq).n * 0c by Def1
.=0c;
end;
hence seq is convergent by COMSEQ_2:9;
thus thesis by A6,COMSEQ_2:9,10;
end;
A7: seq.0= z |^ (0+1) by A2
.=z;
now
A8: 0 <= |.z.| by COMPLEX1:46;
assume |.z.| <> 0;
hence thesis by A1,A7,A3,A8,Th43;
end;
hence thesis by A4;
end;
theorem
r>0 & (ex m st for n st n>=m holds |.seq.n.| >= r) implies not |.seq.|
is convergent or lim |.seq.| <> 0
proof
assume that
A1: r>0 and
A2: ex m st for n st n>=m holds |.seq.n.| >= r;
consider m such that
A3: for n st n>=m holds |.seq.n.| >= r by A2;
now
let n such that
A4: n>=m;
0 <= |.seq.|.n by Lm3;
then |.(|.seq.|).n.| =|.seq.|.n by ABSVALUE:def 1
.=|.seq.n.| by VALUED_1:18;
hence |.(|.seq.|).n.| >= r by A3,A4;
end;
hence thesis by A1,SERIES_1:38;
end;
theorem Th46:
seq is convergent iff for p st 0*

* 0c;
registration
cluster summable for Complex_Sequence;
existence
proof
take D, 0c;
let p be Real such that
A1: 0*

convergent for Complex_Sequence; coherence by Def8; end; definition let seq be Complex_Sequence; attr seq is absolutely_summable means :Def9: |.seq.| is summable; end; theorem Th51: (for n holds seq.n = 0c) implies seq is absolutely_summable proof assume A1: for n holds seq.n = 0c; take 0; let p be Real such that A2: 0

summable for Real_Sequence;
coherence by Def9;
end;
theorem Th52:
seq is summable implies seq is convergent & lim seq = 0c
proof
assume
A1: seq is summable;
then Re Partial_Sums(seq) is convergent;
then Partial_Sums(Re seq) is convergent by Th26;
then
A2: Re seq is summable;
Im Partial_Sums(seq) is convergent by A1;
then Partial_Sums(Im seq) is convergent by Th26;
then
A3: Im seq is summable;
then lim(Im seq)=0 by SERIES_1:4;
then
A4: Im(lim(seq))=0 by A2,A3,Th42;
lim(Re seq)=0 by A2,SERIES_1:4;
then Re(lim(seq))=0 by A2,A3,Th42;
hence thesis by A2,A3,A4,Lm1,Th42,COMPLEX1:13;
end;
registration
cluster summable -> convergent for Complex_Sequence;
coherence by Th52;
end;
theorem Th53:
seq is summable implies Re seq is summable & Im seq is summable
& Sum(seq)= Sum(Re seq)+Sum(Im seq)**
proof
A1: lim(Re Partial_Sums(seq))=lim(Partial_Sums(Re seq)) & lim(Im
Partial_Sums( seq))=lim(Partial_Sums(Im seq)) by Th26;
assume
A2: seq is summable;
then Re Partial_Sums(seq) is convergent;
then
A3: Partial_Sums(Re seq) is convergent by Th26;
Im Partial_Sums(seq) is convergent by A2;
then
A4: Partial_Sums(Im seq) is convergent by Th26;
lim(Re Partial_Sums(seq))=Re(lim(Partial_Sums(seq))) & lim(Im
Partial_Sums( seq))=Im(lim(Partial_Sums(seq))) by A2,Th41;
hence thesis by A3,A4,A1,COMPLEX1:13;
end;
registration
let seq be summable Complex_Sequence;
cluster Re seq -> summable for Real_Sequence;
coherence by Th53;
cluster Im seq -> summable for Real_Sequence;
coherence by Th53;
end;
theorem Th54:
seq1 is summable & seq2 is summable implies seq1+seq2 is
summable & Sum(seq1+seq2)= Sum(seq1)+Sum(seq2)
proof
assume
A1: seq1 is summable & seq2 is summable;
then
A2: Partial_Sums(seq1)+Partial_Sums(seq2) is convergent;
A3: Partial_Sums(seq1)+Partial_Sums(seq2) =Partial_Sums(seq1+seq2) by Th27;
Sum(seq1+seq2)=lim(Partial_Sums(seq1)+Partial_Sums(seq2)) by Th27
.=lim(Partial_Sums(seq1))+lim(Partial_Sums(seq2)) by A1,COMSEQ_2:14;
hence thesis by A2,A3;
end;
theorem Th55:
seq1 is summable & seq2 is summable implies seq1-seq2 is
summable & Sum(seq1-seq2)= Sum(seq1)-Sum(seq2)
proof
assume
A1: seq1 is summable & seq2 is summable;
then
A2: Partial_Sums(seq1)-Partial_Sums(seq2) is convergent;
A3: Partial_Sums(seq1)-Partial_Sums(seq2) =Partial_Sums(seq1-seq2) by Th28;
Sum(seq1-seq2)=lim(Partial_Sums(seq1)-Partial_Sums(seq2)) by Th28
.=lim(Partial_Sums(seq1))-lim(Partial_Sums(seq2)) by A1,COMSEQ_2:26;
hence thesis by A2,A3;
end;
registration
let seq1, seq2 be summable Complex_Sequence;
cluster seq1 + seq2 -> summable for Complex_Sequence;
coherence by Th54;
cluster seq1 - seq2 -> summable for Complex_Sequence;
coherence by Th55;
end;
theorem Th56:
seq is summable implies for z being Complex holds z (#)
seq is summable & Sum(z (#) seq)= z * Sum(seq)
proof
assume
A1: seq is summable;
let z be Complex;
A2: Partial_Sums(z (#) seq)=(z (#) Partial_Sums(seq)) by Th29;
Sum(z (#) seq)=lim((z (#) Partial_Sums(seq))) by Th29
.=z * Sum(seq) by A1,COMSEQ_2:18;
hence thesis by A1,A2;
end;
registration
let z be Element of COMPLEX, seq be summable Complex_Sequence;
cluster z (#) seq -> summable for Complex_Sequence;
coherence by Th56;
end;
theorem Th57:
Re seq is summable & Im seq is summable implies seq is summable
& Sum(seq)=Sum(Re seq)+Sum(Im seq)*
proof
assume that
A1: Re seq is summable and
A2: Im seq is summable;
Partial_Sums(Im seq) is convergent by A2;
then
A3: Im Partial_Sums(seq) is convergent by Th26;
Partial_Sums(Re seq) is convergent by A1;
then
A4: Re Partial_Sums(seq) is convergent by Th26;
then
A5: lim(Im Partial_Sums(seq))=Im(lim(Partial_Sums(seq))) by A3,Th42;
A6: lim(Re Partial_Sums(seq))=lim(Partial_Sums(Re seq)) & lim(Im
Partial_Sums( seq))=lim(Partial_Sums(Im seq)) by Th26;
Partial_Sums(seq) is convergent & lim(Re Partial_Sums(seq))=Re(lim(
Partial_Sums(seq))) by A4,A3,Th42;
hence thesis by A6,A5,COMPLEX1:13;
end;
theorem Th58:
seq is summable implies for n holds seq^\n is summable
proof
assume
A1: seq is summable;
let n;
A2: Re (seq^\n)=Re seq^\n & Im(seq^\n)=Im seq^\n by Th23;
Re seq^\n is summable & Im seq^\n is summable by A1,SERIES_1:12;
hence seq^\n is summable by A2,Th57;
end;
registration
let seq be summable Complex_Sequence, n be Nat;
cluster seq^\n -> summable for Complex_Sequence;
coherence by Th58;
end;
theorem
(ex n st seq^\n is summable) implies seq is summable
proof
given n such that
A1: seq^\n is summable;
Im (seq^\n)=Im seq^\n by Th23;
then
A2: Im seq is summable by A1,SERIES_1:13;
Re (seq^\n)=Re seq^\n by Th23;
then Re seq is summable by A1,SERIES_1:13;
hence thesis by A2,Th57;
end;
theorem
seq is summable implies for n holds Sum(seq) = Partial_Sums(seq).n +
Sum(seq^\(n+1))
proof
assume
A1: seq is summable;
then Sum(seq)=Sum(Re(seq))+(Sum(Im(seq)))* by Th53;
then
A2: Re(Sum(seq))=Sum(Re(seq)) & Im(Sum(seq))=Sum(Im(seq)) by COMPLEX1:12;
let n;
A3: Sum(seq^\(n+1)) = Sum(Re(seq^\(n+1)))+(Sum(Im(seq^\(n+1))))* by A1,Th53;
A4: Sum(Im(seq)) =Partial_Sums(Im(seq)).n + Sum(Im(seq)^\(n+1)) by A1,
SERIES_1:15
.=Im(Partial_Sums(seq)).n + Sum(Im(seq)^\(n+1)) by Th26
.=Im(Partial_Sums(seq)).n + Sum(Im(seq^\(n+1))) by Th23
.=Im(Partial_Sums(seq)).n + Im(Sum(seq^\(n+1))) by A3,COMPLEX1:12
.=Im(Partial_Sums(seq).n) + Im(Sum(seq^\(n+1))) by Def6
.=Im(Partial_Sums(seq).n+ Sum(seq^\(n+1))) by COMPLEX1:8;
Sum(Re(seq)) =Partial_Sums(Re(seq)).n + Sum(Re(seq)^\(n+1)) by A1,SERIES_1:15
.=Re(Partial_Sums(seq)).n + Sum(Re(seq)^\(n+1)) by Th26
.=Re(Partial_Sums(seq)).n + Sum(Re(seq^\(n+1))) by Th23
.=Re(Partial_Sums(seq)).n + Re(Sum(seq^\(n+1))) by A3,COMPLEX1:12
.=Re(Partial_Sums(seq).n) + Re(Sum(seq^\(n+1))) by Def5
.=Re(Partial_Sums(seq).n+ Sum(seq^\(n+1))) by COMPLEX1:8;
hence thesis by A2,A4,COMPLEX1:def 3;
end;
theorem Th61:
Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable
proof
Partial_Sums(|.seq.|) is bounded_above iff |.seq.| is summable;
hence thesis;
end;
registration
let seq be absolutely_summable Complex_Sequence;
cluster Partial_Sums |.seq.| -> bounded_above for Real_Sequence;
coherence by Th61;
end;
theorem Th62:
seq is summable iff for p st 0*

* summable for Complex_Sequence;
coherence by Th63;
end;
registration
cluster absolutely_summable for Complex_Sequence;
existence
proof
set C = the absolutely_summable Complex_Sequence;
take C;
thus thesis;
end;
end;
theorem Th64:
|.z.| < 1 implies z GeoSeq is summable & Sum(z GeoSeq) = 1r/(1r- z)
proof
set seq2 = NAT --> 1r;
deffunc f(Nat) = z |^ ($1+1);
consider seq1 such that
A1: for n holds seq1.n=f(n) from COMSEQ_1:sch 1;
assume
A2: |.z.|<1;
then
A3: lim(seq1)=0c by A1,Th44;
A4: now
let n be Element of NAT;
thus Partial_Sums(z GeoSeq).n = (1r - z |^ (n+1))/(1r-z) by A2,Th36,
COMPLEX1:48
.= (1r - seq1.n)/(1r-z) by A1
.= 1r * (seq2.n-seq1.n)/(1r-z) by COMPLEX1:def 4,FUNCOP_1:7
.= (1r/(1r-z)) * (seq2.n+-seq1.n) by XCMPLX_1:74
.= (1r/(1r-z)) * (seq2.n+(-seq1).n) by VALUED_1:8
.= (1r/(1r-z)) * (seq2-seq1).n by VALUED_1:1
.= ((1r/(1r-z))(#)(seq2-seq1)).n by VALUED_1:6;
end;
A5: for n holds seq2.n=1r
by ORDINAL1:def 12,FUNCOP_1:7;
then
A6: seq2 is convergent by COMSEQ_2:9;
A7: seq1 is convergent by A2,A1,Th44;
then
A8: seq2-seq1 is convergent by A6;
hence Partial_Sums(z GeoSeq) is convergent by A4,FUNCT_2:63;
lim(seq2-seq1)=lim(seq2)-lim(seq1) by A7,A6,COMSEQ_2:26
.=1r by A3,A5,COMSEQ_2:10;
then lim((1r/(1r-z))(#)(seq2-seq1))=1r/(1r-z) * 1r by A8,COMSEQ_2:18
.=1r/(1r-z) by COMPLEX1:def 4;
hence thesis by A4,FUNCT_2:63;
end;
theorem
|.z.| < 1 & (for n holds seq.(n+1) = z * seq.n) implies seq is
summable & Sum(seq) = seq.0/(1r-z)
proof
assume that
A1: |.z.|< 1 and
A2: for n holds seq.(n+1) = z * seq.n;
now
let n be Element of NAT;
thus Partial_Sums(seq).n = seq.0 * ((1r - z |^ (n+1))/(1r-z)) by A1,A2,Th37
,COMPLEX1:48
.=seq.0 * Partial_Sums(z GeoSeq).n by A1,Th36,COMPLEX1:48
.=(seq.0 (#) Partial_Sums(z GeoSeq)).n by VALUED_1:6;
end;
then
A3: Partial_Sums(seq)=(seq.0 (#) Partial_Sums(z GeoSeq));
A4: z GeoSeq is summable by A1,Th64;
hence seq is summable by A3;
Sum seq=seq.0 * Sum(z GeoSeq) by A3,A4,COMSEQ_2:18
.=seq.0 * (1r/(1r-z)) by A1,Th64
.=seq.0 * 1r/(1r-z) by XCMPLX_1:74
.=seq.0/(1r-z) by COMPLEX1:def 4;
hence thesis;
end;
theorem
rseq1 is summable & (ex m st for n st m<=n holds |.seq2.n.| <= rseq1.n
) implies seq2 is absolutely_summable
proof
assume that
A1: rseq1 is summable and
A2: ex m st for n st m<=n holds |.seq2.n.| <= rseq1.n;
consider m such that
A3: for n st m<=n holds |.seq2.n.| <= rseq1.n by A2;
A4: now
let n;
|.seq2.n.|=|.seq2.|.n by VALUED_1:18;
hence 0 <= |.seq2.|.n by COMPLEX1:46;
end;
now
let n;
assume m <= n;
then |.seq2.n.| <= rseq1.n by A3;
hence |.seq2.|.n <= rseq1.n by VALUED_1:18;
end;
hence |.seq2.| is summable by A1,A4,SERIES_1:19;
end;
theorem
(for n holds 0 <= |.seq1.|.n & |.seq1.|.n <= |.seq2.|.n) & seq2 is
absolutely_summable implies seq1 is absolutely_summable & Sum |.seq1.| <= Sum
|.seq2.|
by SERIES_1:20;
theorem
(for n holds |.seq.|.n>0) & (ex m st for n st n>=m holds |.seq.|.(n+1)
/|.seq.|.n >= 1) implies not seq is absolutely_summable by SERIES_1:27;
theorem
(for n holds rseq1.n = n-root (|.seq.|.n)) & rseq1 is convergent & lim
rseq1 < 1 implies seq is absolutely_summable
proof
assume
A1: ( for n holds rseq1.n = n-root (|.seq.|.n))& rseq1 is convergent &
lim rseq1 < 1;
for n holds |.seq.|.n >=0 by Lm3;
hence |.seq.| is summable by A1,SERIES_1:28;
end;
theorem
(for n holds rseq1.n = n-root (|.seq.|.n)) & (ex m st for n st m<=n
holds rseq1.n>= 1) implies |.seq.| is not summable
proof
assume
A1: ( for n holds rseq1.n = n-root (|.seq.|.n))& ex m st for n st m<=n
holds rseq1 .n>= 1;
for n holds |.seq.|.n >=0 by Lm3;
hence thesis by A1,SERIES_1:29;
end;
theorem
(for n holds rseq1.n = n-root (|.seq.|.n)) & rseq1 is convergent & lim
rseq1 > 1 implies seq is not absolutely_summable
proof
assume
A1: ( for n holds rseq1.n = n-root (|.seq.|.n))& rseq1 is convergent &
lim rseq1 > 1;
for n holds |.seq.|.n >=0 by Lm3;
hence |.seq.| is not summable by A1,SERIES_1:30;
end;
theorem
|.seq .| is non-increasing & (for n holds rseq1.n = 2 to_power n * |.
seq.|.(2 to_power n)) implies (seq is absolutely_summable iff rseq1 is summable
)
proof
assume |.seq.| is non-increasing & for n holds rseq1.n = 2 to_power n * |.
seq.|.(2 to_power n);
then for n holds |.seq.| is non-increasing & |.seq.|.n >= 0 & rseq1.n = 2
to_power n * |.seq.|.(2 to_power n) by Lm3;
then |.seq.| is summable iff rseq1 is summable by SERIES_1:31;
hence thesis;
end;
theorem
p>1 & (for n st n>=1 holds |.seq.|.n = 1/n to_power p) implies seq is
absolutely_summable
by SERIES_1:32;
theorem
p<=1 & (for n st n>=1 holds |.seq.|.n=1/n to_power p) implies not seq
is absolutely_summable by SERIES_1:33;
theorem
(for n holds seq.n<>0c & rseq1.n=|.seq.|.(n+1)/|.seq.|.n) & rseq1 is
convergent & lim rseq1 < 1 implies seq is absolutely_summable
proof
assume that
A1: for n holds seq.n<>0c & rseq1.n=|.seq.|.(n+1)/|.seq.|.n and
A2: rseq1 is convergent & lim rseq1 < 1;
now
let n;
A3: seq.n<>0c & |.seq.|.n =|.seq.n.| by A1,VALUED_1:18;
hence |.seq.|.n <>0 & rseq1.n=|.seq.|.(n+1)/|.seq.|.n by A1,COMPLEX1:47;
thus (|.seq.|).n <>0 & rseq1.n=|.(|.seq.|).|.(n+1)/|.seq.|.n by A1,A3,
COMPLEX1:47;
thus (|.seq.|).n <>0 & rseq1.n=abs((|.seq.|)).(n+1)/abs((|.seq.|)).n by A1
,A3,COMPLEX1:47;
end;
then |.seq.| is absolutely_summable by A2,SERIES_1:37;
hence thesis;
end;
theorem
(for n holds seq.n<>0c) & (ex m st for n st n>=m holds |.seq.|.(n+1)/
|.seq.|.n >= 1) implies seq is not absolutely_summable
proof
assume that
A1: for n holds seq.n<>0c and
A2: ex m st for n st n>=m holds |.seq.|.(n+1)/|.seq.|.n >= 1;
consider m such that
A3: for n st n>=m holds |.seq.|.(n+1)/|.seq.|.n >= 1 by A2;
A4: now
let n;
seq.n<>0c by A1;
then |.seq.n.|<>0 by COMPLEX1:47;
hence |.seq.|.n <>0 by VALUED_1:18;
end;
for n st n>=m holds abs((|.seq.|)).(n+1)/abs((|.seq.|)).n >= 1 by A3;
hence |.seq.| is not summable by A4,SERIES_1:39;
end;
*