Copyright (c) 1997 Association of Mizar Users
environ
vocabulary SEQ_1, COMSEQ_1, COMPLEX1, FUNCT_1, SERIES_1, ABSVALUE, ARYTM,
ARYTM_1, SUPINF_2, SEQ_2, ARYTM_3, PROB_1, ORDINAL2, SEQM_3, PREPOWER,
SQUARE_1, RLVECT_1, RELAT_1, POWER, LATTICES;
notation SUBSET_1, ORDINAL1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, REAL_1,
RELAT_1, FUNCT_2, SEQ_1, SEQ_2, NAT_1, SEQM_3, ABSVALUE, SERIES_1,
COMPLEX1, COMSEQ_1, COMSEQ_2, SQUARE_1, POWER;
constructors SEQ_2, SEQM_3, SERIES_1, SQUARE_1, COMSEQ_1, COMSEQ_2, REAL_1,
NAT_1, ABSVALUE, PARTFUN1, COMPLEX1, MEMBERED, ARYTM_0, ARYTM_3, FUNCT_4;
clusters XREAL_0, COMSEQ_2, SEQ_1, COMSEQ_1, RELSET_1, SEQM_3, NAT_1,
COMPLEX1, MEMBERED, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions SEQ_2, COMSEQ_2, SERIES_1;
theorems AXIOMS, NAT_1, REAL_1, ABSVALUE, SEQ_1, SEQ_2, SERIES_1, SEQM_3,
SEQ_4, POWER, COMPLEX1, COMSEQ_1, COMSEQ_2, SQUARE_1, FUNCT_2, XREAL_0,
XCMPLX_0, XCMPLX_1, ARYTM_0;
schemes NAT_1, SEQ_1, COMSEQ_1, RECDEF_1;
begin :: Preliminaries
reserve rseq,rseq1,rseq2 for Real_Sequence;
reserve seq,seq1,seq2 for Complex_Sequence;
reserve k, n, n1, n2, m for Nat;
reserve p,r for Real;
L0: 0c = [*0,0*] by ARYTM_0:def 7;
theorem
[*(n+1),0*] <> 0c & [*0,(n+1)*] <> 0c by ARYTM_0:12,L0;
theorem Th2:
(for n holds rseq.n = 0) implies for m holds (Partial_Sums abs(rseq)).m = 0
proof
assume
A1: for n holds rseq.n = 0;
let m;
defpred P[Nat] means abs(rseq).$1 = (Partial_Sums abs(rseq)).$1;
A2: P[0] by SERIES_1:def 1;
A3: for k st P[k] holds P[k+1]
proof let k be Nat such that
A4: P[k];
thus abs(rseq).(k+1) = 0 + abs(rseq).(k+1)
.= abs(0) + abs(rseq).(k+1) by ABSVALUE:def 1
.= abs(rseq.k) + abs(rseq).(k+1) by A1
.= (Partial_Sums abs(rseq)).k + abs(rseq).(k+1) by A4,SEQ_1:16
.= (Partial_Sums abs(rseq)).(k+1) by SERIES_1:def 1;
end;
for n holds P[n] from Ind(A2,A3);
hence (Partial_Sums abs(rseq)).m = abs(rseq).m
.= abs(rseq.m) by SEQ_1:16
.= abs(0) by A1
.= 0 by ABSVALUE:def 1;
end;
theorem Th3:
(for n holds rseq.n = 0) implies rseq is absolutely_summable
proof
assume
A1: for n holds rseq.n = 0;
take 0;
let p be real number such that
A2: 0<p;
take 0;
let m be Nat such that 0<=m;
abs((Partial_Sums abs(rseq)).m-0) = abs(0-0) by A1,Th2
.= 0 by ABSVALUE:def 1;
hence abs((Partial_Sums abs(rseq)).m-0)<p by A2;
end;
deffunc f(set) = 0;
definition
cluster absolutely_summable Real_Sequence;
existence
proof
consider C being Real_Sequence such that
A1: for n being Nat holds C.n = f(n) from ExRealSeq;
take C;
thus thesis by A1,Th3;
end;
end;
definition
cluster summable -> convergent Real_Sequence;
coherence by SERIES_1:7;
end;
definition
cluster absolutely_summable -> summable Real_Sequence;
coherence by SERIES_1:40;
end;
definition
cluster absolutely_summable Real_Sequence;
existence
proof
consider R being absolutely_summable Real_Sequence;
take R;
thus thesis;
end;
end;
theorem
rseq is convergent implies
(for p st 0<p ex n st for m,l be Nat st n <= m & n <= l
holds abs(rseq.m-rseq.l)<p)
proof
assume
A1:rseq is convergent;
let p; assume 0<p;
then 0<p/2 by SEQ_2:3;
then consider n such that
A2:
for m st n <= m holds abs(rseq.m-rseq.n)<p/2 by A1,SEQ_4:58;
take n;
now let m,l be Nat; assume
A3:n <= m & n <= l;
then A4:abs(rseq.m-rseq.n)<p/2 by A2;
abs(rseq.l-rseq.n)<p/2 by A2,A3;
then abs(rseq.m-rseq.n)+abs(rseq.l-rseq.n) < p/2+p/2 by A4,REAL_1:67;
then A5:abs(rseq.m-rseq.n)+abs(rseq.l-rseq.n) < p by XCMPLX_1:66;
abs(rseq.m-rseq.l) = abs((rseq.m-rseq.n)-(rseq.l-rseq.n))
by XCMPLX_1:22;
then abs(rseq.m-rseq.l) <= abs(rseq.m-rseq.n)+abs(rseq.l-rseq.n)
by ABSVALUE:19;
hence abs(rseq.m-rseq.l) < p by A5,AXIOMS:22;
end;
hence for m,l be Nat st n <= m & n <= l holds abs(rseq.m-rseq.l)<p;
end;
theorem
(for n holds rseq.n <= p) implies for n, l be Nat holds
Partial_Sums(rseq).(n+l)-Partial_Sums(rseq).n <= p * l
proof
assume
A1:for n holds rseq.n <= p;
now let n;
defpred P[Nat] means Partial_Sums(rseq).(n+$1)-Partial_Sums(rseq).n <= p * $1;
Partial_Sums(rseq).(n+0)-Partial_Sums(rseq).n
=Partial_Sums(rseq).n+-Partial_Sums(rseq).n by XCMPLX_0:def 8
.=p * 0 by XCMPLX_0:def 6;
then A2: P[0];
A3:
now let l be Nat such that
A4: P[l];
A5:
Partial_Sums(rseq).(n+(l+1))-Partial_Sums(rseq).n
=Partial_Sums(rseq).((n+l)+1)-Partial_Sums(rseq).n
by XCMPLX_1:1
.=Partial_Sums(rseq).((n+l))+rseq.(n+l+1)-Partial_Sums(rseq).n
by SERIES_1:def 1
.=Partial_Sums(rseq).((n+l))-Partial_Sums(rseq).n+rseq.(n+l+1)
by XCMPLX_1:29;
A6:
rseq.(n+l+1) <= p by A1;
A7:
Partial_Sums(rseq).(n+(l+1))-Partial_Sums(rseq).n
<= p * l + rseq.(n+l+1) by A4,A5,AXIOMS:24;
A8:
p * l + rseq.(n+l+1) <= p * l + p by A6,AXIOMS:24;
p * l + p=p * l + p * 1
.=p * (l+1) by XCMPLX_1:8;
hence P[l+1] by A7,A8,AXIOMS:22;
end;
thus for l be Nat holds P[l] from Ind(A2,A3);
end;
hence thesis;
end;
theorem
(for n holds rseq.n <= p) implies
for n holds Partial_Sums(rseq).n <= p * (n+1)
proof
defpred P[Nat] means Partial_Sums(rseq).$1 <= p * ($1+1);
assume
A1:for n holds rseq.n <= p;
Partial_Sums(rseq).(0) =rseq.0 by SERIES_1:def 1;
then A2:P[0] by A1;
A3:
now let n be Nat such that
A4: P[n];
A5: Partial_Sums(rseq).(n+1)
=Partial_Sums(rseq).(n)+rseq.(n+1)
by SERIES_1:def 1;
A6: rseq.(n+1) <= p by A1;
A7: Partial_Sums(rseq).(n+1)
<= p * (n+1) + rseq.(n+1) by A4,A5,AXIOMS:24;
A8: p * (n+1)+ rseq.(n+1) <= p * (n+1) + p by A6,AXIOMS:24;
p * (n+1) + p=p * (n+1) + p * 1
.=p * ((n+1)+1) by XCMPLX_1:8;
hence P[n+1] by A7,A8,AXIOMS:22;
end;
thus for n be Nat holds P[n] from Ind(A2,A3);
end;
theorem
(for n st n <= m holds rseq1.n <= p * rseq2.n) implies
Partial_Sums(rseq1).m <= p * Partial_Sums(rseq2).m
proof
assume
A1: for n st n <= m holds rseq1.n <= p * rseq2.n;
defpred P[Nat] means $1 <= m implies Partial_Sums(rseq1).$1 <=
p * Partial_Sums(rseq2).$1;
A2: P[0] proof assume
A3: 0 <= m;
A4: Partial_Sums(rseq1).(0) =rseq1.0 by SERIES_1:def 1;
p * Partial_Sums(rseq2).(0) =p * rseq2.0 by SERIES_1:def 1;
hence thesis by A1,A3,A4;
end;
A5:
now let n be Nat such that
A6: P[n];
now assume
A7: n + 1 <= m;
A8: n < n+1 by REAL_1:69;
A9: Partial_Sums(rseq1).(n+1) =Partial_Sums(rseq1).(n)+rseq1.(n+1)
by SERIES_1:def 1;
A10: rseq1.(n+1) <= p * rseq2.(n+1) by A1,A7;
A11: Partial_Sums(rseq1).(n+1)
<= p * Partial_Sums(rseq2).(n) +
rseq1.(n+1) by A6,A7,A8,A9,AXIOMS:22,24;
A12: p * Partial_Sums(rseq2).(n) + rseq1.(n+1)
<= p * Partial_Sums(rseq2).(n) + p * rseq2.(n+1)
by A10,AXIOMS:24;
p * Partial_Sums(rseq2).(n) + p * rseq2.(n+1)
=p * (Partial_Sums(rseq2).(n) +rseq2.(n+1)) by XCMPLX_1:8
.=p * Partial_Sums(rseq2).(n+1) by SERIES_1:def 1;
hence Partial_Sums(rseq1).(n+1)
<= p * Partial_Sums(rseq2).(n+1) by A11,A12,AXIOMS:22;
end;
hence P[n+1];
end;
for n be Nat holds P[n] from Ind(A2,A5);
hence Partial_Sums(rseq1).(m) <= p * Partial_Sums(rseq2).(m);
end;
theorem
(for n st n <= m holds rseq1.n <= p * rseq2.n) implies
for n st n <= m holds
for l be Nat st n+l <= m holds
Partial_Sums(rseq1).(n+l)-Partial_Sums(rseq1).n
<= p * (Partial_Sums(rseq2).(n+l)-Partial_Sums(rseq2).n)
proof
assume
A1: for n st n <= m holds rseq1.n <= p * rseq2.n;
let n such that n <= m;
defpred P[Nat] means n+$1 <= m implies
Partial_Sums(rseq1).(n+$1)-Partial_Sums(rseq1).n
<= p * (Partial_Sums(rseq2).(n+$1)-Partial_Sums(rseq2).n);
A2: P[0] proof assume
n+0 <= m;
A3: Partial_Sums(rseq1).(n+0)-Partial_Sums(rseq1).(n)
=Partial_Sums(rseq1).(n)+-Partial_Sums(rseq1).(n) by XCMPLX_0:def 8
.=0 by XCMPLX_0:def 6;
p *( Partial_Sums(rseq2).(n+0)-Partial_Sums(rseq2).(n))
=p * (Partial_Sums(rseq2).(n)+-Partial_Sums(rseq2).(n)) by XCMPLX_0:
def 8
.=p * 0 by XCMPLX_0:def 6;
hence thesis by A3;
end;
A4: for l be Nat st P[l] holds P[l+1]
proof let l be Nat such that
A5: P[l];
assume n + (l+1) <= m;
then A6: n+l+1 <= m by XCMPLX_1:1;
A7: n+l < (n+l)+1 by REAL_1:69;
A8: Partial_Sums(rseq1).(n+(l+1))
=Partial_Sums(rseq1).(n+l+1) by XCMPLX_1:1
.=Partial_Sums(rseq1).(n+l)+rseq1.(n+l+1) by SERIES_1:def 1;
rseq1.(n+l+1) <= p * rseq2.(n+l+1) by A1,A6;
then Partial_Sums(rseq1).(n+(l+1))
<= Partial_Sums(rseq1).(n+l) + p * rseq2.(n+l+1) by A8,AXIOMS:24;
then A9: Partial_Sums(rseq1).(n+(l+1))-Partial_Sums(rseq1).n
<= Partial_Sums(rseq1).(n+l) + p * rseq2.(n+l+1)
-Partial_Sums(rseq1).n by REAL_1:49;
A10: Partial_Sums(rseq1).(n+l) + p * rseq2.(n+l+1)
-Partial_Sums(rseq1).n =
Partial_Sums(rseq1).(n+l) -Partial_Sums(rseq1).n
+ p * rseq2.(n+l+1) by XCMPLX_1:29;
A11:
Partial_Sums(rseq1).(n+l) -Partial_Sums(rseq1).n
+ p * rseq2.(n+l+1)
<= p * (Partial_Sums(rseq2).(n+l)-Partial_Sums(rseq2).n)
+ p * rseq2.(n+l+1) by A5,A6,A7,AXIOMS:22,24;
p * (Partial_Sums(rseq2).(n+l)-Partial_Sums(rseq2).n)
+ p * rseq2.(n+l+1)
= p * (Partial_Sums(rseq2).(n+l)-Partial_Sums(rseq2).n
+ rseq2.(n+l+1)) by XCMPLX_1:8
.= p * (Partial_Sums(rseq2).(n+l)+rseq2.(n+l+1)
-Partial_Sums(rseq2).n) by XCMPLX_1:29
.=p * (Partial_Sums(rseq2).((n+l)+1)
-Partial_Sums(rseq2).n)
by SERIES_1:def 1
.=p * (Partial_Sums(rseq2).(n+(l+1))
-Partial_Sums(rseq2).n) by XCMPLX_1:1;
hence thesis by A9,A10,A11,AXIOMS:22;
end;
thus for l be Nat holds P[l] from Ind(A2,A4);
end;
theorem
(for n holds 0 <= rseq.n) implies
(for n, m st n <= m holds
abs(Partial_Sums(rseq).m-Partial_Sums(rseq).n)
=Partial_Sums(rseq).m-Partial_Sums(rseq).n)
&
for n holds abs(Partial_Sums(rseq).n)=Partial_Sums(rseq).n
proof
assume
A1:for n holds 0 <= rseq.n;
then A2:Partial_Sums(rseq) is non-decreasing by SERIES_1:19;
A3:
now let n,m; assume n <= m;
then Partial_Sums(rseq).n <= Partial_Sums(rseq).m by A2,SEQM_3:12;
then Partial_Sums(rseq).n-Partial_Sums(rseq).n
<= Partial_Sums(rseq).m-Partial_Sums(rseq).n by REAL_1:49;
then 0 <= Partial_Sums(rseq).m-Partial_Sums(rseq).n by XCMPLX_1:14;
hence abs(Partial_Sums(rseq).m-Partial_Sums(rseq).n)
=Partial_Sums(rseq).m-Partial_Sums(rseq).n by ABSVALUE:def 1;
end;
now let n;
A4:Partial_Sums(rseq).0 = rseq.0 by SERIES_1:def 1;
A5:0 <= rseq.0 by A1;
0 <= n by NAT_1:18;
then Partial_Sums(rseq).0 <= Partial_Sums(rseq).n by A2,SEQM_3:12;
hence abs(Partial_Sums(rseq).n)=Partial_Sums(rseq).n by A4,A5,ABSVALUE:def 1;
end;
hence thesis by A3;
end;
theorem
seq1 is convergent & seq2 is convergent & lim(seq1-seq2)=0c
implies lim seq1 = lim seq2
proof
assume
A1: seq1 is convergent & seq2 is convergent & lim(seq1-seq2)=0c;
then lim(seq1-seq2)=lim(seq1)-lim(seq2) by COMSEQ_2:26;
hence lim(seq1)=lim(seq2) by A1,XCMPLX_1:15;
end;
begin :: The Operations on Complex Sequences
reserve z for Element of COMPLEX;
reserve Nseq,Nseq1 for increasing Seq_of_Nat;
Lm1:
|.seq.n.|=|.seq.|.n & 0 <= |.seq.|.n
proof
|.seq.n.|=|.seq.|.n by COMSEQ_1:def 14;
hence thesis by COMPLEX1:132;
end;
definition let z be Element of COMPLEX;
func z GeoSeq -> Complex_Sequence means :Def1:
it.0 = 1r & for n holds it.(n+1) = it.n * z;
existence
proof
deffunc f(set,Element of COMPLEX) = $2*z;
consider f being Function of NAT,COMPLEX such that
A1: f.0 = 1r & for n being Nat holds f.(n+1) = f(n,f.n) from LambdaRecExD;
take f;
thus thesis by A1;
end;
uniqueness
proof
let seq1,seq2;
assume that A2: seq1.0=1r & for n holds
seq1.(n+1)=seq1.n * z and
A3: seq2.0=1r & for n holds
seq2.(n+1)=seq2.n * z;
defpred P[Nat] means seq1.$1 = seq2.$1;
A4: P[0] by A2,A3;
A5: 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 A2
.= seq2.(k+1) by A3;
end;
for n holds P[n] from Ind(A4,A5);
hence seq1 = seq2 by COMSEQ_1:6;
end;
end;
definition let z be Element of COMPLEX,
n be Nat;
func z #N n -> Element of COMPLEX equals:Def2:
z GeoSeq.n;
correctness;
end;
theorem
z #N 0 = 1r
proof
thus z #N 0 = (z GeoSeq).0 by Def2
.= 1r by Def1;
end;
definition let c be Complex_Sequence;
func Re c -> Real_Sequence means :Def3:
for n holds it.n = Re(c.n);
existence
proof
deffunc f(Nat) = Re(c.$1);
thus ex f being Real_Sequence st for n holds f.n = f(n) from ExRealSeq;
end;
uniqueness
proof
let seq,seq' be Real_Sequence such that
A1: for n holds seq.n=Re(c.n) and
A2: for n holds seq'.n=Re(c.n);
now let n;
seq.n=Re(c.n) & seq'.n=Re(c.n) by A1,A2;
hence seq.n=seq'.n;
end;
hence seq=seq' by FUNCT_2:113;
end;
end;
definition let c be Complex_Sequence;
func Im c -> Real_Sequence means :Def4:
for n holds it.n = Im(c.n);
existence
proof
deffunc f(Nat) = Im(c.$1);
thus ex f being Real_Sequence st for n holds f.n = f(n) from ExRealSeq;
end;
uniqueness
proof
let seq,seq' be Real_Sequence such that
A1: for n holds seq.n=Im(c.n) and
A2: for n holds seq'.n=Im(c.n);
now let n;
seq.n=Im(c.n) & seq'.n=Im(c.n) by A1,A2;
hence seq.n=seq'.n;
end;
hence seq=seq' by FUNCT_2:113;
end;
end;
theorem Th12:
|.z.| <= abs Re z + abs Im z
proof
A1:z = [*Re z, Im z*] by COMPLEX1:8;
A2:Re([*Re z,0*])=Re z by COMPLEX1:7;
A3:Im([*Re z,0*])=0 by COMPLEX1:7;
A4:Re([*0,Im z*])=0 by COMPLEX1:7;
A5:Im([*0,Im z*])=Im z by COMPLEX1:7;
[*Re z,0*] +[*0,Im z*]
=[*Re ([*Re z,0*])+Re([*0,Im z*]), Im ([*Re z,0*])+Im([*0,Im z*])*]
by COMPLEX1:def 9
.=[*Re z ,Im z*] by A3,A4,A5,COMPLEX1:7;
then A6: |.z.| <= |.[*Re z,0*].| +|.[*0,Im z*].| by A1,COMPLEX1:142;
|.[*Re z,0*].| = abs(Re z) by A2,A3,COMPLEX1:136;
hence thesis by A4,A5,A6,COMPLEX1:137;
end;
theorem Th13:
abs(Re z) <= |.z.| & abs(Im z) <= |.z.|
proof
A1:|.z.| = sqrt ((Re z)^2 + (Im z)^2) by COMPLEX1:def 16;
A2:0 <= (Re z)^2 by SQUARE_1:72;
0 <= (Im z)^2 by SQUARE_1:72;
then 0+(Re z)^2 <= (Im z)^2 + (Re z)^2 by AXIOMS:24;
then A3:0 <= (Re z)^2 & (Re z)^2 <= (Re z)^2 + (Im z)^2 by SQUARE_1:72;
0+(Im z)^2 <= (Re z)^2 + (Im z)^2 by A2,AXIOMS:24;
then A4:0 <= (Im z)^2 & (Im z)^2 <= (Re z)^2 + (Im z)^2 by SQUARE_1:72;
A5:sqrt((Re z)^2) <= sqrt((Re z)^2 + (Im z)^2) by A3,SQUARE_1:94;
sqrt((Im z)^2) <= sqrt((Re z)^2 + (Im z)^2) by A4,SQUARE_1:94;
hence thesis by A1,A5,SQUARE_1:91;
end;
theorem Th14:
Re seq1=Re seq2 & Im seq1=Im seq2 implies seq1=seq2
proof
assume
A1: Re seq1=Re seq2 & Im seq1=Im seq2;
now let n;
A2:Re(seq1.n)=Re seq2.n by A1,Def3
.=Re(seq2.n) by Def3;
Im(seq1.n)=Im seq2.n by A1,Def4
.=Im(seq2.n) by Def4;
hence seq1.n=seq2.n by A2,COMPLEX1:9;
end;
hence seq1=seq2 by COMSEQ_1:6;
end;
theorem Th15:
Re seq1 + Re seq2 = Re (seq1+seq2) &
Im seq1 + Im seq2 = Im (seq1+seq2)
proof
now let n;
thus (Re seq1+Re seq2).n=Re seq1.n+Re seq2.n by SEQ_1:11
.=Re(seq1.n)+Re seq2.n by Def3
.=Re(seq1.n)+Re(seq2.n) by Def3
.=Re(seq1.n+seq2.n) by COMPLEX1:19
.=Re((seq1+seq2).n) by COMSEQ_1:def 4
.=Re (seq1+seq2).n by Def3;
end;
hence
Re seq1+Re seq2=Re (seq1+seq2) by FUNCT_2:113;
now let n;
thus
(Im seq1+Im seq2).n=Im seq1.n+Im seq2.n by SEQ_1:11
.=Im(seq1.n)+Im seq2.n by Def4
.=Im(seq1.n)+Im(seq2.n) by Def4
.=Im(seq1.n+seq2.n) by COMPLEX1:19
.=Im((seq1+seq2).n) by COMSEQ_1:def 4
.=Im (seq1+seq2).n by Def4;
end;
hence Im seq1+Im seq2=Im (seq1+seq2) by FUNCT_2:113;
end;
theorem Th16:
-(Re seq) = Re (-seq) & -(Im seq) = Im -seq
proof
now let n;
thus
(-Re seq).n= -(Re seq.n) by SEQ_1:14
.=-Re(seq.n) by Def3
.= Re(-(seq.n)) by COMPLEX1:34
.= Re((-seq).n) by COMSEQ_1:def 9
.=Re (-seq).n by Def3;
end;
hence -Re seq=Re (-seq) by FUNCT_2:113;
now let n;
thus
(-Im seq).n=-Im seq.n by SEQ_1:14
.=-Im(seq.n) by Def4
.= Im(-(seq.n)) by COMPLEX1:34
.= Im((-seq).n) by COMSEQ_1:def 9
.=(Im -seq).n by Def4;
end;
hence -Im seq=Im -seq by FUNCT_2:113;
end;
theorem Th17:
r*Re(z)=Re([*r,0*]*z) & r*Im(z)=Im([*r,0*]*z)
proof
set zr=[*r,0*];
A1:Re(zr)=r &Im(zr)=0 by COMPLEX1:7;
[*r,0*]*z=[*Re(zr) * Re z - Im(zr) * Im z,Re(zr) * Im z
+ Re z * Im zr *] by COMPLEX1:def 10
.= [*r * Re z,r * Im z*] by A1;
hence thesis by COMPLEX1:7;
end;
theorem Th18:
Re seq1-Re seq2=Re (seq1-seq2) & Im seq1-Im seq2=Im(seq1-seq2)
proof
now let n;
thus
(Re seq1-Re seq2).n = (Re seq1+-Re seq2).n by SEQ_1:15
.= Re seq1.n+(-Re seq2).n by SEQ_1:11
.=Re seq1.n+(Re -seq2).n by Th16
.=(Re seq1+Re -seq2).n by SEQ_1:11
.=Re (seq1+(-seq2)).n by Th15
.=Re (seq1-seq2).n by COMSEQ_1:def 10;
end;
hence
Re seq1-Re seq2=Re (seq1-seq2) by FUNCT_2:113;
now let n;
thus
(Im seq1-Im seq2).n = (Im seq1+-Im seq2).n by SEQ_1:15
.= Im seq1.n+(-Im seq2).n by SEQ_1:11
.=Im seq1.n+Im (-seq2).n by Th16
.=(Im seq1+Im -seq2).n by SEQ_1:11
.=Im (seq1+ -seq2).n by Th15
.=Im(seq1-seq2).n by COMSEQ_1:def 10;
end;
hence Im seq1-Im seq2=Im(seq1-seq2) by FUNCT_2:113;
end;
theorem
r(#)Re seq = Re ([*r,0*] (#) seq) & r(#)Im seq = Im ([*r,0*] (#) seq)
proof
now let n;
thus
(r(#)Re seq).n= r*(Re seq.n) by SEQ_1:13
.=r*Re(seq.n) by Def3
.=Re([*r,0*]*(seq.n)) by Th17
.=Re(([*r,0*] (#) seq).n) by COMSEQ_1:def 7
.=Re ([*r,0*] (#) seq).n by Def3;
end;
hence r(#)Re seq=Re ([*r,0*] (#) seq) by FUNCT_2:113;
now let n;
thus
(r(#)Im seq).n= r*(Im seq.n) by SEQ_1:13
.=r*Im(seq.n) by Def4
.=Im([*r,0*]*(seq.n)) by Th17
.=Im(([*r,0*] (#) seq).n) by COMSEQ_1:def 7
.=Im([*r,0*](#)seq).n by Def4;
end;
hence r(#)Im seq=Im([*r,0*](#)seq) by FUNCT_2:113;
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;
thus
Re (z (#) seq).n=Re((z (#) seq).n) by Def3
.=Re((z * seq.n )) by COMSEQ_1:def 7
.=Re([*Re(z) * Re(seq.n) - Im(z) * Im(seq.n),
Re(z) * Im(seq.n) + Re(seq.n) * Im(z)*])
by COMPLEX1:def 10
.= Re(z) * Re(seq.n) - Im(z) * Im(seq.n) by COMPLEX1:7
.= Re(z) *( Re seq.n) - Im(z) * Im(seq.n)
by Def3
.= Re(z) *( Re seq.n) - Im(z) *( Im seq.n)
by Def4
.= (Re(z) (#) Re seq).n - Im(z) *( Im seq.n)
by SEQ_1:13
.= (Re(z) (#) Re seq).n - (Im(z) (#) Im seq).n
by SEQ_1:13
.= (Re(z) (#) Re seq).n + (- (Im(z) (#) Im seq).n)
by XCMPLX_0:def 8
.= (Re(z) (#) Re seq).n + (- Im(z) (#) Im seq).n
by SEQ_1:14
.= (Re(z) (#) Re seq +(- Im(z) (#) Im seq)).n
by SEQ_1:11
.= (Re(z) (#) Re seq - Im(z) (#) Im seq).n
by SEQ_1:15;
end;
hence
Re (z (#) seq)=Re(z)(#)Re seq-Im(z)(#)Im seq by FUNCT_2:113;
now let n;
thus
Im(z(#)seq).n =Im((z (#) seq).n) by Def4
.=Im((z * seq.n )) by COMSEQ_1:def 7
.=Im([*Re(z) * Re(seq.n) - Im(z) * Im(seq.n),
Re(z) * Im(seq.n) + Re(seq.n) * Im(z)*])
by COMPLEX1:def 10
.= Re(z) * Im(seq.n) + Re(seq.n) * Im(z) by COMPLEX1:7
.= Re(z) * Im(seq.n) + Im(z) * Re seq.n
by Def3
.= Re(z) * Im seq.n + Im(z) *( Re seq.n)
by Def4
.= (Re(z) (#) Im seq).n + Im(z) *( Re seq.n)
by SEQ_1:13
.= (Re(z) (#) Im seq).n + (Im(z) (#) Re seq).n
by SEQ_1:13
.= (Re(z) (#) Im seq + Im(z) (#) Re seq).n
by SEQ_1:11;
end;
hence
Im(z(#)seq)=Re(z)(#)Im seq+Im(z)(#)Re seq by FUNCT_2:113;
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;
thus
Re (seq1 (#) seq2).n=Re((seq1 (#) seq2).n) by Def3
.=Re((seq1.n * seq2.n )) by COMSEQ_1:def 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:def 10
.= Re(seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n)
by COMPLEX1:7
.= (Re seq1.n) * Re(seq2.n) - Im(seq1.n) * Im(seq2.n)
by Def3
.= (Re seq1.n) *( Re seq2.n) - Im(seq1.n) * Im(seq2.n)
by Def3
.= (Re seq1.n) *( Re seq2.n) - Im(seq1.n) *( Im seq2.n)
by Def4
.= (Re seq1.n) *( Re seq2.n) - (Im seq1.n)*( Im seq2.n)
by Def4
.= (Re seq1 (#) Re seq2).n - (Im seq1.n) *( Im seq2.n)
by SEQ_1:12
.= (Re seq1 (#) Re seq2).n - (Im seq1 (#) Im seq2).n
by SEQ_1:12
.= (Re seq1 (#)Re seq2).n + (- (Im seq1 (#) Im seq2).n)
by XCMPLX_0:def 8
.= (Re seq1 (#) Re seq2).n + (- Im seq1 (#) Im seq2).n
by SEQ_1:14
.= (Re seq1 (#) Re seq2 +(- Im seq1 (#) Im seq2)).n
by SEQ_1:11
.= (Re seq1 (#) Re seq2 - Im seq1 (#) Im seq2).n
by SEQ_1:15;
end;
hence Re (seq1 (#) seq2)=Re seq1(#)Re seq2-Im seq1(#)Im seq2 by FUNCT_2:113
;
now let n;
thus
Im (seq1 (#) seq2).n =Im((seq1 (#) seq2).n) by Def4
.=Im((seq1.n * seq2.n )) by COMSEQ_1:def 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:def 10
.= Re(seq1.n) * Im(seq2.n) + Re(seq2.n) * Im(seq1.n)
by COMPLEX1:7
.= Re(seq1.n) * Im(seq2.n) + Im(seq1.n) * Re seq2.n
by Def3
.= Re seq1.n * Im(seq2.n) + Im(seq1.n) * Re seq2.n
by Def3
.= Re seq1.n * Im seq2.n + Im(seq1.n) * Re seq2.n
by Def4
.= (Re seq1.n * Im seq2.n) + (Im seq1.n * Re seq2.n)
by Def4
.= (Re seq1 (#) Im seq2).n + Im seq1.n *( Re seq2.n)
by SEQ_1:12
.= (Re seq1 (#) Im seq2).n + (Im seq1 (#) Re seq2).n
by SEQ_1:12
.= (Re seq1 (#) Im seq2 + Im seq1 (#) Re seq2).n
by SEQ_1:11;
end;
hence
Im (seq1 (#) seq2)=Re seq1(#)Im seq2+Im seq1(#)Re seq2 by FUNCT_2:113;
end;
definition let seq be Complex_Sequence,
Nseq be increasing Seq_of_Nat;
func seq (#) Nseq -> Complex_Sequence means :Def5:
for n holds it.n = seq.(Nseq.n);
existence
proof
deffunc f(Nat) = seq.(Nseq.$1);
thus ex f being Complex_Sequence st for n holds f.n = f(n) from ExComplexSeq;
end;
uniqueness
proof
let seq1,seq2 be Complex_Sequence such
that
A1: for n holds seq1.n= seq.(Nseq.n) and
A2: for n holds seq2.n=seq.(Nseq.n);
now let n;
seq1.n=seq.(Nseq.n) & seq2.n=seq.(Nseq.n) by A1,A2;
hence seq1.n=seq2.n;
end;
hence seq1=seq2 by COMSEQ_1:6;
end;
end;
theorem Th22:
Re (seq(#)Nseq)=(Re seq)*Nseq & Im (seq(#)Nseq)=(Im seq)*Nseq
proof
now let n;
thus
(Re (seq(#)Nseq)).n =Re((seq(#)Nseq).n) by Def3
.=Re(seq.(Nseq.n)) by Def5
.=Re seq.(Nseq.n) by Def3
.=(Re seq*Nseq).n by SEQM_3:31;
end;
hence
Re (seq(#)Nseq)=Re seq*Nseq by FUNCT_2:113;
now let n;
thus
Im (seq(#)Nseq).n =Im((seq(#)Nseq).n) by Def4
.=Im(seq.(Nseq.n)) by Def5
.=Im seq.(Nseq.n) by Def4
.=(Im seq*Nseq).n by SEQM_3:31;
end;
hence Im (seq(#)Nseq)=Im seq*Nseq by FUNCT_2:113;
end;
definition let seq be Complex_Sequence,
k be Nat;
func seq ^\ k -> Complex_Sequence means :Def6:
for n holds it.n=seq.(n+k);
existence
proof
deffunc f(Nat) = seq.($1+k);
thus ex f being Complex_Sequence st for n holds f.n = f(n) from ExComplexSeq;
end;
uniqueness
proof
let seq1,seq2;
assume that A1:for n holds seq1.n=seq.(n+k) and
A2:for n holds seq2.n=seq.(n+k);
now let n;
seq1.n=seq.(n+k) & seq2.n=seq.(n+k) by A1,A2;
hence seq1.n=seq2.n;
end;
hence seq1=seq2 by COMSEQ_1:6;
end;
end;
theorem Th23:
(Re seq)^\k =Re (seq^\k) & (Im seq)^\k =Im (seq^\k)
proof
now let n;
thus (Re seq^\k).n =Re seq.(n+k)
by SEQM_3:def 9
.=Re(seq.(n+k)) by Def3
.=Re((seq^\k).n)
by Def6
.=Re ((seq)^\k).n by Def3;
thus (Im seq^\k).n =Im seq.(n+k)
by SEQM_3:def 9
.=Im(seq.(n+k)) by Def4
.=Im((seq^\k).n)
by Def6
.=Im ((seq)^\k).n by Def4;
end;
hence (Re seq)^\k =Re ((seq)^\k) & (Im seq)^\k =Im ((seq)^\k) by FUNCT_2:113;
end;
definition let seq be Complex_Sequence;
func Partial_Sums seq -> Complex_Sequence means :Def7:
it.0 = seq.0 & for n holds it.(n+1) = it.n + seq.(n+1);
existence
proof
deffunc f(Nat,Element of COMPLEX) = $2 + seq.($1+1);
consider f being Function of NAT,COMPLEX such that
A1: f.0 = seq.0 & for n being Nat holds f.(n+1) = f(n,f.n) from LambdaRecExD;
take f;
thus thesis by A1;
end;
uniqueness
proof
let seq1,seq2;
assume that A2: seq1.0=seq.0 & for n holds
seq1.(n+1)=seq1.n + seq.(n+1) and
A3: seq2.0=seq.0 & for n holds
seq2.(n+1)=seq2.n + seq.(n+1);
defpred P[Nat] means seq1.$1 = seq2.$1;
A4: P[0] by A2,A3;
A5: 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 + seq.(k+1) by A2
.= seq2.(k+1) by A3;
end;
for n holds P[n] from Ind(A4,A5);
hence seq1 = seq2 by COMSEQ_1:6;
end;
end;
definition let seq be Complex_Sequence;
func Sum seq -> Element of COMPLEX equals :Def8:
lim Partial_Sums seq;
correctness;
end;
theorem Th24:
(for n holds seq.n = 0c) implies for m holds (Partial_Sums seq).m = 0c
proof
assume
A1: for n holds seq.n = 0c;
let m;
defpred P[Nat] means seq.$1 = (Partial_Sums seq).$1;
A2: P[0] by Def7;
A3: for k st P[k] holds P[k+1]
proof let k be Nat such that
A4: P[k];
thus seq.(k+1) = 0c + seq.(k+1) by COMPLEX1:22
.= (Partial_Sums seq).k + seq.(k+1) by A1,A4
.= (Partial_Sums seq).(k+1) by Def7;
end;
for n holds P[n] from Ind(A2,A3);
then seq = Partial_Sums seq by COMSEQ_1:6;
hence (Partial_Sums seq).m = 0c by A1;
end;
theorem Th25:
(for n holds seq.n = 0c) implies for m holds (Partial_Sums |.seq.|).m = 0
proof
assume
A1: for n holds seq.n = 0c;
let m;
defpred P[Nat] means |.seq.|.$1 = (Partial_Sums |.seq.|).$1;
A2: P[0] by SERIES_1:def 1;
A3: for k st P[k] holds P[k+1]
proof let k be Nat such that
A4: P[k];
thus |.seq.|.(k+1) = |.0c.| + |.seq.|.(k+1) by COMPLEX1:130
.= |.seq.k.| + |.seq.|.(k+1) by A1
.= (Partial_Sums |.seq.|).k + |.seq.|.(k+1) by A4,
COMSEQ_1:def 14
.= (Partial_Sums |.seq.|).(k+1) by SERIES_1:def 1;
end;
for n holds P[n] from Ind(A2,A3);
hence (Partial_Sums |.seq.|).m = |.seq.|.m
.= |.seq.m.| by COMSEQ_1:def 14
.= 0 by A1,COMPLEX1:130;
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;
A1:P[0] proof thus Partial_Sums(Re seq).0 = Re seq.0 by SERIES_1:def 1
.= Re(seq.0) by Def3
.= Re(Partial_Sums(seq).0) by Def7
.= Re Partial_Sums(seq).0 by Def3;
end;
A2: 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 Def3
.=Re(Partial_Sums(seq).k) +Re(seq.(k+1)) by Def3
.=Re(Partial_Sums(seq).k + seq.(k+1)) by COMPLEX1:19
.=Re(Partial_Sums(seq).(k+1)) by Def7
.=Re Partial_Sums(seq).(k+1) by Def3;
hence thesis;
end;
A3:for n holds P[n] from Ind(A1,A2);
defpred R[Nat] means Partial_Sums(Im seq).$1 = Im Partial_Sums(seq).$1;
A4:R[0] proof thus Partial_Sums(Im seq).0 = Im seq.0 by SERIES_1:def 1
.= Im(seq.0) by Def4
.= Im(Partial_Sums(seq).0) by Def7
.= Im Partial_Sums(seq).0 by Def4;
end;
A5: 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 Def4
.=Im(Partial_Sums(seq).k) +Im(seq.(k+1)) by Def4
.=Im(Partial_Sums(seq).k + seq.(k+1)) by COMPLEX1:19
.=Im(Partial_Sums(seq).(k+1)) by Def7
.=Im Partial_Sums(seq).(k+1) by Def4;
hence thesis;
end;
for n holds R[n] from Ind(A4,A5);
hence thesis by A3,FUNCT_2:113;
end;
theorem Th27:
Partial_Sums(seq1)+Partial_Sums(seq2) = Partial_Sums(seq1+seq2)
proof
A1:Re (Partial_Sums(seq1)+Partial_Sums(seq2))
=Re Partial_Sums(seq1)+Re Partial_Sums(seq2) by Th15
.=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:8
.=Partial_Sums(Re (seq1+seq2)) by Th15
.=Re Partial_Sums(seq1+seq2) by Th26;
Im (Partial_Sums(seq1)+Partial_Sums(seq2))
=Im Partial_Sums(seq1)+Im Partial_Sums(seq2) by Th15
.=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:8
.=Partial_Sums(Im (seq1+seq2)) by Th15
.=Im Partial_Sums(seq1+seq2) by Th26;
hence thesis by A1,Th14;
end;
theorem Th28:
Partial_Sums(seq1)-Partial_Sums(seq2) = Partial_Sums(seq1-seq2)
proof
A1: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:9
.=Partial_Sums(Re (seq1-seq2)) by Th18
.=Re Partial_Sums(seq1-seq2) by Th26;
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:9
.=Partial_Sums(Im (seq1-seq2)) by Th18
.=Im Partial_Sums(seq1-seq2) by Th26;
hence thesis by A1,Th14;
end;
theorem Th29:
Partial_Sums(z (#) seq) = z (#) Partial_Sums(seq)
proof
defpred P[Nat] means Partial_Sums(z (#) seq).$1= (z (#) Partial_Sums(seq)).$1;
A1:P[0]
proof
thus Partial_Sums(z(#)seq).0
=(z (#) seq).0 by Def7
.=z * seq.0 by COMSEQ_1:def 7
.=z * Partial_Sums(seq).0 by Def7
.=(z (#) Partial_Sums(seq)).0 by COMSEQ_1:def 7;
end;
A2:now let n;
assume
A3: P[n];
thus P[n+1]
proof
thus Partial_Sums(z (#) seq).(n+1)
=Partial_Sums(z (#) seq).n + (z (#) seq).(n+1) by Def7
.=(z * Partial_Sums(seq).n )+ (z (#) seq).(n+1) by A3,COMSEQ_1:def 7
.=(z * Partial_Sums(seq).n )+ (z * seq.(n+1)) by COMSEQ_1:def 7
.= z * ( Partial_Sums(seq).n + seq.(n+1)) by XCMPLX_1:8
.= z * ( Partial_Sums(seq).(n+1)) by Def7
.= (z (#) Partial_Sums(seq)).(n+1) by COMSEQ_1:def 7;
end;
end;
for n holds P[n] from Ind(A1,A2);
hence thesis by COMSEQ_1:6;
end;
theorem
|.Partial_Sums(seq).k.| <= Partial_Sums(|.seq.|).k
proof
defpred P[Nat] means |. Partial_Sums(seq).$1 .|
<= Partial_Sums(|.seq.|).$1;
Partial_Sums(|.seq.|).0
= (|.seq.|).0 by SERIES_1:def 1
.= |. seq.0 .| by COMSEQ_1:def 14;
then A1: P[0] by Def7;
A2:
now let k such that
A3: P[k];
A4: |. Partial_Sums(seq).(k+1) .|
=|. Partial_Sums(seq).k + (seq).(k+1) .| by Def7;
A5: |. Partial_Sums(seq).k + (seq).(k+1) .|
<= |. Partial_Sums(seq).k.| + |. (seq).(k+1) .| by COMPLEX1:142;
|. Partial_Sums(seq).k.| + |.(seq).(k+1).|
<= Partial_Sums(|.seq.| ).k + |.(seq).(k+1).|
by A3,AXIOMS:24;
then |. Partial_Sums(seq).(k+1) .| <=
Partial_Sums(|.seq.|).k + |.seq.(k+1).| by A4,A5,AXIOMS:22;
then |. Partial_Sums(seq).(k+1) .|
<= Partial_Sums(|.seq.|).k+|.seq.|.(k+1) by COMSEQ_1:def 14;
hence P[k+1] by SERIES_1:def 1;
end;
for k holds P[k] from Ind(A1,A2);
hence thesis;
end;
theorem Th31:
|.Partial_Sums(seq).m- Partial_Sums(seq).n.|
<= abs( 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;
Partial_Sums(|.seq.|).(n+0)-Partial_Sums(|.seq.|).n
=Partial_Sums(|.seq.|).n+-Partial_Sums(|.seq.|).n
by XCMPLX_0:def 8
.=0 by XCMPLX_0:def 6;
then A2: P[0];
A3:
now let k be Nat;
assume
A4: P[k];
A5: Partial_Sums(|.seq.|).(n+(k+1))- Partial_Sums(|.seq.|).n
=Partial_Sums(|.seq.|).((n+k)+1)- Partial_Sums(|.seq.|).n
by XCMPLX_1:1
.=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 COMSEQ_1:def 14
.=Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n
+|.seq.(n+k+1).| by XCMPLX_1:29;
0 <= |.seq.(n+k+1).| by COMPLEX1:132;
then 0+0 <= Partial_Sums(|.seq.|).(n+k)
- Partial_Sums(|.seq.|).n
+|.seq.(n+k+1).| by A4,REAL_1:55;
hence P[k+1] by A5;
end;
thus for k be Nat holds P[k] from Ind(A2,A3);
end;
A6:
for n,k be Nat holds
abs( Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n )
= Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n
proof
let n,k be Nat;
0 <= Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n
by A1;
hence thesis by ABSVALUE:def 1;
end;
A7:
for n for m st n <= m holds
|.Partial_Sums(seq).m- Partial_Sums(seq).n.|
<= abs( Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n )
proof
let n;
A8: for k be Nat holds
|.Partial_Sums(seq).(n+k)- Partial_Sums(seq).n.|
<= abs( Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n )
proof
defpred P[Nat] means |.Partial_Sums(seq).(n+$1)- Partial_Sums(seq).n.|
<= abs( Partial_Sums(|.seq.|).(n+$1)- Partial_Sums(|.seq.|).n );
|.Partial_Sums(seq).(n+0)- Partial_Sums(seq).n.| = 0
by COMPLEX1:130,XCMPLX_1:14;
then A9:P[0] by ABSVALUE:5;
A10:
now let k be Nat;
assume
A11: P[k];
A12: |.Partial_Sums(seq).(n+(k+1))- Partial_Sums(seq).n .|
=|.Partial_Sums(seq).((n+k)+1)- Partial_Sums(seq).n .|
by XCMPLX_1:1
.=|.(Partial_Sums(seq).(n+k)+seq.(n+k+1))- Partial_Sums(seq).n.|
by Def7
.=|.Partial_Sums(seq).(n+k)- Partial_Sums(seq).n+seq.(n+k+1).|
by XCMPLX_1:29;
A13:|.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:142;
A14: |.Partial_Sums(seq).(n+k)- Partial_Sums(seq).n.|
+|.seq.(n+k+1).| <=
abs( Partial_Sums(|.seq.|).(n+k)- Partial_Sums(|.seq.|).n )
+|.seq.(n+k+1).| by A11,AXIOMS:24;
abs( 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 by XCMPLX_1:29
.=Partial_Sums(|.seq.|).(n+k)+|.seq.|.(n+k+1)
- Partial_Sums(|.seq.|).n
by COMSEQ_1:def 14
.=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 XCMPLX_1:1
.=abs( Partial_Sums(|.seq.|).(n+(k+1))- Partial_Sums(|.seq.|).n )
by A6;
hence P[k+1] by A12,A13,A14,AXIOMS:22;
end;
thus for k be Nat holds P[k] from Ind(A9,A10);
end;
let m;
assume n <= m;
then consider k be Nat such that
A15:m=n+k by NAT_1:28;
thus thesis by A8,A15;
end;
for n, m holds
|.Partial_Sums(seq).m- Partial_Sums(seq).n.|
<= abs( Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n )
proof
let n,m;
m <= n implies
|.Partial_Sums(seq).m- Partial_Sums(seq).n.|
<= abs( Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n )
proof
assume m <= n;
then A16:|.Partial_Sums(seq).n- Partial_Sums(seq).m.|
<= abs( Partial_Sums(|.seq.|).n- Partial_Sums(|.seq.|).m )
by A7;
abs( Partial_Sums(|.seq.|).n- Partial_Sums(|.seq.|).m )
=abs(-( Partial_Sums(|.seq.|).n- Partial_Sums(|.seq.|).m) )
by ABSVALUE:17
.=abs( Partial_Sums(|.seq.|).m- Partial_Sums(|.seq.|).n )
by XCMPLX_1:143;
hence thesis by A16,COMPLEX1:146;
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;
thus (Partial_Sums(Re seq)^\k).n =Partial_Sums(Re seq).(n+k)
by SEQM_3:def 9
.=Re Partial_Sums(seq).(n+k) by Th26
.=Re(Partial_Sums(seq).(n+k)) by Def3
.=Re((Partial_Sums(seq)^\k).n)
by Def6
.=(Re (Partial_Sums(seq)^\k)).n by Def3;
thus (Partial_Sums(Im seq)^\k).n =Partial_Sums(Im seq).(n+k)
by SEQM_3:def 9
.=Im Partial_Sums(seq).(n+k) by Th26
.=Im(Partial_Sums(seq).(n+k)) by Def4
.=Im((Partial_Sums(seq)^\k).n)
by Def6
.=Im (Partial_Sums(seq)^\k).n by Def4;
end;
hence thesis by FUNCT_2:113;
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 Def3
.=Re(seq.0) by A1
.=Re seq.0 by Def3;
thus Im seq1.n=Im(seq1.n) by Def4
.=Im(seq.0) by A1
.=Im seq.0 by Def4;
end;
A3: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:14
.=Re (Partial_Sums(seq)^\1)-Re seq1
by Th32
.=Re (Partial_Sums(seq)^\1-seq1)
by Th18;
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:14
.=Im (Partial_Sums(seq)^\1)-Im seq1
by Th32
.=Im (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 Lm1;
hence thesis by SERIES_1:19;
end;
definition let seq be Complex_Sequence;
cluster Partial_Sums |.seq.| -> non-decreasing;
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
assume
A1: for n st n <= m holds seq1.n = seq2.n;
defpred P[Nat] means $1 <= m implies
Partial_Sums(seq1).$1=Partial_Sums(seq2).$1;
A2: P[0] proof assume
A3: 0 <= m;
thus Partial_Sums(seq1).0=seq1.0 by Def7
.=seq2.0 by A1,A3
.=Partial_Sums(seq2).0 by Def7;
end;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A5: P[k];
assume
A6:k+1 <= m;
k < k+1 by REAL_1:69;
hence Partial_Sums(seq1).(k+1)
=Partial_Sums(seq2).k+seq1.(k+1) by A5,A6,Def7,AXIOMS:22
.=Partial_Sums(seq2).k+seq2.(k+1) by A1,A6
.=Partial_Sums(seq2).(k+1) by Def7;
end;
for k holds P[k] from Ind(A2,A4);
hence Partial_Sums(seq1).m=Partial_Sums(seq2).m;
end;
theorem Th36:
1r <> z implies
for n holds Partial_Sums(z GeoSeq).n = (1r - z #N (n+1))/(1r-z)
proof
now
let z;
assume 1r <> z;
then 0< |.1r-z.| by COMPLEX1:148;
then A1: 1r-z <>0c by COMPLEX1:133;
defpred P[Nat] means Partial_Sums(z GeoSeq).$1 = (1r - z #N ($1+1))/(1r-z);
A2:P[0]
proof
thus Partial_Sums(z GeoSeq).0
=(z GeoSeq).0 by Def7
.=1r by Def1
.=(1r-z)/(1r-z) by A1,COMPLEX1:86
.=(1r -1r * z )/(1r-z) by COMPLEX1:29
.=(1r-(z GeoSeq).0 * z)/(1r-z) by Def1
.=(1r -(z GeoSeq).(0+1) )/(1r-z) by Def1
.=(1r-z #N (0+1) )/(1r-z) by Def2;
end;
A3:for n st P[n] holds P[n+1]
proof let n;
assume
A4:P[n];
thus
Partial_Sums(z GeoSeq).(n+1)
=Partial_Sums(z GeoSeq).n + (z GeoSeq).(n+1) by Def7
.= (1r - z #N (n+1))/(1r-z)+ z #N (n+1) by A4,Def2
.= (1r - z #N (n+1))/(1r-z)+ z #N (n+1) * 1r by COMPLEX1:29
.= (1r - z #N (n+1))/(1r-z)+ z #N (n+1) * ((1r-z)/(1r-z))
by A1,COMPLEX1:86
.= (1r - z #N (n+1))/(1r-z)+ (z #N (n+1) * (1r-z))/(1r-z)
by XCMPLX_1:75
.= (1r - z #N (n+1) + (z #N (n+1) * (1r-z)))/(1r-z)
by XCMPLX_1:63
.= (1r - z #N (n+1) + (z #N (n+1) * 1r -z #N(n+1) * z ))/(1r-z)
by XCMPLX_1:40
.= (1r - z #N (n+1) + (z #N (n+1) -z #N(n+1) * z ))/(1r-z)
by COMPLEX1:29
.= (1r - z #N (n+1) + z #N (n+1) -z #N(n+1) * z )/(1r-z)
by XCMPLX_1:29
.= (1r - (z #N (n+1) - z #N (n+1)) -z #N(n+1) * z )/(1r-z)
by XCMPLX_1:37
.= (1r - 0c -z #N(n+1) * z )/(1r-z) by XCMPLX_1:14
.= (1r - z #N(n+1) * z )/(1r-z) by COMPLEX1:52
.= (1r - (z GeoSeq).(n+1) * z )/(1r-z) by Def2
.= (1r - (z GeoSeq).((n+1)+1) )/(1r-z) by Def1
.= (1r - z #N ((n+1) +1) )/(1r-z) by Def2;
end;
thus
for n holds P[n] from Ind(A2,A3);
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 (n+1))/(1r-z))
proof
assume
A1:z <> 1r & for n holds seq.(n+1) = z * seq.n;
defpred P[Nat] means seq.$1=seq.0 * (z GeoSeq).$1;
A2: P[0]
proof
thus seq.0 = seq.0 * 1r by COMPLEX1:29
.= seq.0 * (z GeoSeq).0 by Def1;
end;
A3:
now let n;
assume
A4:P[n];
thus P[n+1]
proof thus seq.(n+1)=z * (seq.0 * (z GeoSeq).n) by A1,A4
.=seq.0 * (z * (z GeoSeq).n) by XCMPLX_1:4
.=seq.0 * (z GeoSeq).(n+1) by Def1;
end;
end;
A5: dom seq = NAT by FUNCT_2:def 1;
for n holds P[n] from Ind(A2,A3);
then A6:Partial_Sums(seq)=Partial_Sums(seq.0 (#) (z GeoSeq)) by A5,COMSEQ_1:def
7
.=seq.0 (#) Partial_Sums(z GeoSeq) by Th29;
let n;
thus Partial_Sums(seq).n=seq.0 * Partial_Sums(z GeoSeq).n
by A6,COMSEQ_1:def 7
.=seq.0 * ( (1r - z #N (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 number such that
A4: for p being real number st 0<p ex n st for m st
n<=m
holds abs(a.m-a1) < p by A2,SEQ_2:def 6;
consider b1 being real number such that
A5: for p being real number st 0<p ex n st for m st n<=m
holds abs(b.m-b1)<p by A3,SEQ_2:def 6;
reconsider a1,b1 as Real by XREAL_0:def 1;
take g=[*a1,b1*];
for p st 0<p holds ex n st for m
st n <= m holds |.c.m-g.|< p
proof
let p be Real; assume 0 < p;
then A6: 0 < p/2 by SEQ_2:3;
then consider n1 such that
A7: for m st n1<=m holds abs(a.m-a1)< p/2 by A4;
consider n2 such that
A8: for m st n2<=m holds abs(b.m-b1)< p/2 by A5,A6;
n1 <= (n1+n2) &n2 <= (n1+n2) by NAT_1:29;
then consider n such that
A9: n1 <= n &n2 <= n;
take n;
for m st n <= m holds |.c.m-g.|< p
proof
let m; assume n <= m;
then n1 <= m & n2 <= m by A9,AXIOMS:22;
then abs(a.m-a1)< p/2 & abs(b.m-b1)< p/2 by A7,A8;
then abs(a.m-a1) + abs(b.m-b1)< p/2+ p/2 by REAL_1:67;
then A10: abs(a.m-a1) + abs(b.m-b1)< p by XCMPLX_1:66;
A11: |.c.m-g.| <= abs(Re(c.m-g)) + abs(Im(c.m-g)) by Th12;
A12: Re(c.m)=a.m by A1;
Re(g) =a1 by COMPLEX1:7;
then A13: Re(c.m-g)=a.m-a1 by A12,COMPLEX1:48;
A14: Im(c.m)=b.m by A1;
Im(g) =b1 by COMPLEX1:7;
then Im(c.m-g)=b.m-b1 by A14,COMPLEX1:48;
hence |.c.m-g.|< p by A10,A11,A13,AXIOMS:22;
end;
hence thesis;
end;
hence thesis;
end;
assume c is convergent;
then consider z such that A15:
for p st 0<p ex n st for m st
n <= m holds |.c.m-z.| < p by COMSEQ_2:def 4;
thus a is convergent
proof
reconsider z as Element of COMPLEX;
take Re(z);
let p be real number;
A16: p is Real by XREAL_0:def 1;
assume 0<p;
then consider n such that
A17: for m st n <= m holds |.c.m-z.| < p by A15,A16;
take n;
let m; assume n <= m;
then A18: |.c.m-z.| < p by A17;
A19: Re(c.m) =a.m by A1;
Re(c.m-z)=Re(c.m)-Re(z) by COMPLEX1:48;
then abs(a.m-Re(z)) <= |.c.m-z.| by A19,Th13;
hence thesis by A18,AXIOMS:22;
end;
take Im(z);
let p be real number;
A20: p is Real by XREAL_0:def 1;
assume p>0;
then consider n such that
A21: for m st
n <= m holds |.c.m-z.| < p by A15,A20;
take n;
let m; assume
n <= m;
then A22: |.c.m-z.| < p by A21;
A23: Im(c.m) =b.m by A1;
Im(c.m-z)=Im(c.m)-Im(z) by COMPLEX1:48;
then abs(b.m-Im(z) ) <= |.c.m-z.| by A23,Th13;
hence thesis by A22,AXIOMS:22;
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; assume
A1: for n holds Re(c.n) = a.n & Im(c.n) = b.n;
hence
A2: c is convergent by Th38;
set g=[*lim(a),lim(b)*];
for p st 0<p holds ex n st for m st n<=m holds |.c.m-g.|< p
proof
let p be Real;
assume 0 < p;
then A3: 0 < p/2 by SEQ_2:3;
then consider n1 such that
A4: for m st n1<=m holds abs(a.m-lim(a))< p/2 by SEQ_2:def 7;
consider n2 such that
A5: for m st n2<=m holds abs(b.m-lim(b))< p/2
by A3,SEQ_2:def 7;
n1 <= (n1+n2) &n2 <= (n1+n2) by NAT_1:29;
then consider n such that
A6: n1 <= n &n2 <= n;
take n;
let m; assume n <= m;
then n1 <= m & n2 <= m by A6,AXIOMS:22;
then abs(a.m-lim(a))< p/2 & abs(b.m-lim(b))< p/2 by A4,A5;
then abs(a.m-lim(a)) + abs(b.m-lim(b))< p/2+ p/2 by REAL_1:67;
then A7: abs(a.m-lim(a)) + abs(b.m-lim(b))< p by XCMPLX_1
:66;
A8: |.c.m-g.| <= abs(Re(c.m-g)) + abs(Im(c.m-g)) by Th12;
A9: Re(c.m)=a.m by A1;
Re(g) =lim(a) by COMPLEX1:7;
then A10: Re(c.m-g)=a.m-lim(a) by A9,COMPLEX1:48;
A11: Im(c.m)=b.m by A1;
Im(g) =lim(b) by COMPLEX1:7;
then Im(c.m-g)=b.m-lim(b) by A11,COMPLEX1:48;
hence thesis by A7,A8,A10,AXIOMS:22;
end;
hence thesis by A2,COMSEQ_2:def 5;
end;
theorem Th40:
for a, b being Real_Sequence, c being convergent Complex_Sequence
st (for n holds Re (c.n) = a.n & Im (c.n) = b.n)
holds a is convergent & b is convergent
& lim(a)=Re(lim(c)) & lim(b)=Im (lim(c))
proof
let a, b be Real_Sequence,
c be convergent Complex_Sequence; assume
A1: for n holds Re(c.n) = a.n & Im(c.n) = b.n;
then A2: a is convergent & b is convergent by Th38;
A3: for p being real number st 0<p ex n st for m st n<=m holds
abs(a.m-Re(lim(c)))<p
proof
let p be real number;
A4: p is Real by XREAL_0:def 1;
assume 0<p;
then consider n such that
A5: for m st n <= m holds |.c.m-lim(c).| < p
by A4,COMSEQ_2:def 5;
take n;
let m; assume n <= m;
then A6: |.c.m-lim(c).| < p by A5;
Re(c.m) =a.m by A1;
then Re(c.m-lim(c))=a.m-Re(lim(c)) by COMPLEX1:48;
then abs(a.m-Re(lim(c)) ) <= |.c.m-lim(c).| by Th13;
hence thesis by A6,AXIOMS:22;
end;
for p being real number st 0<p ex n st for m st n<=m holds
abs(b.m-Im(lim(c))) <p
proof
let p be real number;
A7: p is Real by XREAL_0:def 1;
assume p>0;
then consider n such that
A8: for m st
n <= m holds |.c.m-lim(c).| < p by A7,COMSEQ_2:def 5;
take n;
let m; assume
n <= m;
then A9: |.c.m-lim(c).| < p by A8;
A10: Im(c.m) =b.m by A1;
Im(c.m-lim(c))=Im(c.m)-Im(lim(c)) by COMPLEX1:48;
then abs(b.m-Im(lim(c)) ) <= |.c.m-lim(c).| by A10,Th13;
hence thesis by A9,AXIOMS:22;
end;
hence thesis by A2,A3,SEQ_2:def 7;
end;
theorem Th41:
for c being convergent Complex_Sequence holds
Re c is convergent & Im c is convergent
& lim(Re c)=Re(lim(c)) & lim(Im c)=Im (lim(c))
proof
let c be convergent Complex_Sequence;
A1:for n holds Re c.n=Re(c.n) by Def3;
for n holds Im c.n=Im(c.n) by Def4;
hence thesis by A1,Th40;
end;
definition let c be convergent Complex_Sequence;
cluster Re c -> convergent;
coherence by Th41;
cluster Im c -> convergent;
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) by Def3;
for n holds Im c.n=Im(c.n) by Def4;
then c is convergent & lim(c)=[*lim(Re c),lim(Im c)*] by A1,A2,Th39;
hence thesis by COMPLEX1:7;
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 A1:
0 < |.z.| & |.z.| < 1;
assume A2:
seq.0 = z & for n holds seq.(n+1) = seq.n * z;
A3: for n holds |.seq.n.| = |.z.| to_power (n+1)
proof
defpred P[Nat] means |. seq.$1 .|= |.z.| to_power ($1+1);
A4: P[0] by A2,POWER:30;
A5: for k st P[k] holds P[k+1]
proof
let k be Nat;
assume
A6: P[k];
|.seq.(k+1).| = |.seq.k * z.| by A2
.= |.z.| to_power (k+1) * |.z.| by A6,COMPLEX1:151
.= |.z.| to_power (k+1) * |.z.| to_power (1)
by POWER:30
.= |.z.| to_power ((k+1)+1) by A1,POWER:32;
hence |.seq.(k+1).| = |.z.| to_power ((k+1)+1);
end;
for n holds P[n] from Ind(A4,A5);
hence thesis;
end;
consider rseq be Real_Sequence such that
A7:for n holds rseq.n=f(n) from ExRealSeq;
A8:rseq is constant by A7,SEQM_3:def 6;
rseq.0=0 by A7;
then A9: rseq is convergent & lim(rseq)=0 by A8,SEQ_4:39,40;
deffunc g(Nat) = |.z.| to_power ($1+1);
consider rseq1 such that A10:
for n holds rseq1.n=g(n) from ExRealSeq;
A11: rseq1 is convergent & lim(rseq1)=0 by A1,A10,SERIES_1:1;
A12: (for n holds rseq.n <= abs(Re seq).n )
& (for n holds abs(Re seq).n <= rseq1.n)
proof
A13: now let n;
0 <= abs(Re seq).n
proof
abs(Re seq).n=abs(Re seq.n) by SEQ_1:16;
hence thesis by ABSVALUE:5;
end;
hence rseq.n <= abs(Re seq).n by A7;
end;
now let n;
abs(Re seq).n = abs(Re seq.n) by SEQ_1:16;
then A14: abs(Re seq).n = abs(Re(seq.n)) by Def3;
A15: abs(Re(seq.n)) <= |.seq.n.| by Th13;
|.seq.n.| = |.z.| to_power (n+1) by A3;
hence abs(Re seq).n <= rseq1.n by A10,A14,A15;
end;
hence thesis by A13;
end;
A16: (for n holds rseq.n <= abs(Im seq).n )
& (for n holds abs(Im seq).n <= rseq1.n)
proof
A17:
now let n;
0 <= abs(Im seq).n
proof
abs(Im seq).n=abs(Im seq.n) by SEQ_1:16;
hence thesis by ABSVALUE:5;
end;
hence rseq.n <= abs(Im seq).n by A7;
end;
now let n;
A18: abs(Im seq).n = abs(Im seq.n) by SEQ_1:16;
A19: abs(Im(seq.n)) <= |.seq.n.| by Th13;
|.seq.n.| = |.z.| to_power (n+1) by A3;
then abs(Im seq).n <= |.z.| to_power (n+1)
by A18,A19,Def4;
hence abs(Im seq).n <= rseq1.n by A10;
end;
hence thesis by A17;
end;
A20: abs(Re seq) is convergent by A9,A11,A12,SEQ_2:33;
A21: lim(abs(Re seq))=0 by A9,A11,A12,SEQ_2:34;
A22:abs(Im seq) is convergent by A9,A11,A16,SEQ_2:33;
A23:lim(abs(Im seq))=0 by A9,A11,A16,SEQ_2:34;
A24: Re seq is convergent & lim(Re seq)=0 by A20,A21,SEQ_4:28;
Im seq is convergent & lim(Im seq)=0 by A22,A23,SEQ_4:28;
then seq is convergent & Re lim(seq)=0 &Im lim(seq)=0 by A24,Th42;
hence thesis by COMPLEX1:8,L0;
end;
theorem Th44:
|.z.| < 1 & (for n holds seq.n=z #N (n+1))
implies seq is convergent & lim(seq)=0c
proof
assume
A1: |.z.| <1 & (for n holds seq.n=z #N (n+1));
then A2:
seq.0= z #N (0+1)
.=(z GeoSeq).(0+1) by Def2
.=(z GeoSeq).0 * z by Def1
.=1r * z by Def1
.=z by COMPLEX1:29;
A3:
now let n;
thus
seq.(n+1) = z #N ((n+1)+1) by A1
.= (z GeoSeq).((n+1)+1) by Def2
.= (z GeoSeq).(n+1) * z by Def1
.= z #N (n+1) * z by Def2
.= seq.n * z by A1;
end;
A4:
now
assume
A5: |.z.| <> 0;
0 <= |.z.| by COMPLEX1:132;
hence seq is convergent & lim(seq)=0c by A1,A2,A3,A5,Th43;
end;
now
assume
|.z.| = 0;
then A6: z =0c by COMPLEX1:131;
A7:
now let n;
thus
seq.n = 0c #N (n+1) by A1,A6
.=(0c GeoSeq).(n+1) by Def2
.=(0c GeoSeq).n * 0c by Def1
.=0c by COMPLEX1:28;
end;
hence seq is convergent by COMSEQ_2:9;
thus seq is convergent & lim(seq)=0c by A7,COMSEQ_2:9,10;
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
A1: r>0 & (ex m st for n st n>=m holds |.seq.n.| >= r);
then consider m such that
A2: for n st n>=m holds |.seq.n.| >= r;
now let n such that
A3:n>=m;
0 <= |.seq.|.n by Lm1;
then abs((|.seq.|).n) =|.seq.|.n by ABSVALUE:def 1
.=|.seq.n.| by COMSEQ_1:def 14;
hence abs((|.seq.|).n) >= r by A2,A3;
end;
hence thesis by A1,SERIES_1:43;
end;
theorem Th46:
seq is convergent iff
for p st 0<p ex n st for m st n <= m holds |.seq.m-seq.n.|<p
proof
A1:now
assume seq is convergent;
then consider z such that
A2:for p st 0<p holds ex n st
for m st n <= m holds |.seq.m-z.|<p by COMSEQ_2:def 4;
let p; assume
0< p;
then 0 <p/2 by SEQ_2:3;
then consider n such that
A3: for m st n <= m holds |.seq.m-z.|<p/2 by A2;
take n;
let m; assume
n <= m;
then A4:|.seq.m-z.|<p/2 by A3;
|.seq.n-z.|<p/2 by A3;
then |.seq.m-z.| + |.seq.n-z.| <p/2+p/2 by A4,REAL_1:67;
then |.seq.m-z.| + |.seq.n-z.| <p by XCMPLX_1:66;
then A5:|.seq.m-z.| + |.z-seq.n.| <p by COMPLEX1:146;
|.seq.m-seq.n.| <= |.seq.m-z.| + |.z-seq.n.| by COMPLEX1:149;
hence |.seq.m-seq.n.|< p by A5,AXIOMS:22;
end;
now assume
A6: for p st 0<p holds ex n st for m st n <= m holds |.seq.m-seq.n.|<p;
for p be real number st 0<p holds ex n st for m st n <= m
holds abs(Re seq.m-Re seq.n)<p
proof
let p be real number;
A7: p is Real by XREAL_0:def 1;
assume 0<p;
then consider n such that
A8: for m st n <= m holds |.seq.m-seq.n.|<p by A6,A7;
take n;
let m; assume
n <= m;
then A9: |.seq.m-seq.n.|<p by A8;
Re(seq.m-seq.n)=Re(seq.m)-Re(seq.n) by COMPLEX1:48
.=Re seq.m-Re(seq.n) by Def3
.=Re seq.m-Re seq.n by Def3;
then abs(Re seq.m-Re seq.n) <= |.seq.m-seq.n.| by Th13;
hence abs(Re seq.m-Re seq.n) < p by A9,AXIOMS:22;
end;
hence
A10: Re seq is convergent by SEQ_4:58;
for p be real number st 0<p holds ex n st for m st n <= m
holds abs(Im seq.m-Im seq.n)<p
proof
let p be real number;
A11: p is Real by XREAL_0:def 1;
assume 0<p;
then consider n such that
A12: for m st n <= m holds |.seq.m-seq.n.|<p by A6,A11;
take n;
let m; assume
n <= m;
then A13: |.seq.m-seq.n.|<p by A12;
Im(seq.m-seq.n)=Im(seq.m)-Im(seq.n) by COMPLEX1:48
.=Im seq.m-Im(seq.n) by Def4
.=Im seq.m-Im seq.n by Def4;
then abs(Im seq.m-Im seq.n) <= |.seq.m-seq.n.| by Th13;
hence abs(Im seq.m-Im seq.n) < p by A13,AXIOMS:22;
end;
hence Im seq is convergent by SEQ_4:58;
hence seq is convergent by A10,Th42;
end;
hence thesis by A1;
end;
theorem
seq is convergent implies
(for p st 0<p ex n st for m,l be Nat st n <= m & n <= l
holds |.seq.m-seq.l.|<p)
proof
assume
A1: seq is convergent;
let p; assume
0<p;
then 0<p/2 by SEQ_2:3;
then consider n such that
A2:
for m st n <= m holds |.seq.m-seq.n.|<p/2 by A1,Th46;
take n;
now let m,l be Nat; assume
A3:n <= m & n <= l;
then A4:|.seq.m-seq.n.|<p/2 by A2;
|.seq.l-seq.n.|<p/2 by A2,A3;
then |.seq.m-seq.n.|+|.seq.l-seq.n.| < p/2+p/2 by A4,REAL_1:67;
then A5:|.seq.m-seq.n.|+|.seq.l-seq.n.| < p by XCMPLX_1:66;
A6:
|.(seq.m-seq.n)-(seq.l-seq.n).|
=|.seq.m-seq.n-seq.l+seq.n.| by XCMPLX_1:37
.=|.seq.m+-seq.n-seq.l+seq.n.| by XCMPLX_0:def 8
.=|.seq.m+-seq.n+-seq.l+seq.n.| by XCMPLX_0:def 8
.=|.seq.m+-seq.l+-seq.n+seq.n.| by XCMPLX_1:1
.=|.(seq.m+-seq.l)+(-seq.n+seq.n).| by XCMPLX_1:1
.=|.(seq.m+-seq.l)+0c.| by XCMPLX_0:def 6
.=|.(seq.m+-seq.l).| by COMPLEX1:22
.=|.(seq.m-seq.l).| by XCMPLX_0:def 8;
|.(seq.m-seq.n)-(seq.l-seq.n).|
<= |.seq.m-seq.n.|+|.seq.l-seq.n.| by COMPLEX1:143;
hence |.seq.m-seq.l.| < p by A5,A6,AXIOMS:22;
end;
hence thesis;
end;
theorem
((for n holds |. seq.n .| <= rseq.n)
& rseq is convergent & lim(rseq)=0)
implies seq is convergent & lim(seq)=0c
proof
assume
A1: (for n holds |. seq.n .| <= rseq.n) & rseq is convergent & lim(rseq)=0;
ex rseq1 be Real_Sequence st for n holds rseq1.n = f(n) from ExRealSeq;
then consider rseq1 be Real_Sequence such that
A2:for n holds rseq1.n=0;
A3:rseq1 is constant by A2,SEQM_3:def 6;
rseq1.0=0 by A2;
then A4: rseq1 is convergent & lim(rseq1)=0 by A3,SEQ_4:39,40;
A5: (for n holds rseq1.n <= abs(Re(seq)).n )
& (for n holds abs(Re(seq)).n <= rseq.n)
proof
A6: now let n;
0 <= abs(Re(seq)).n
proof
abs(Re(seq)).n=abs(Re(seq).n) by SEQ_1:16;
hence thesis by ABSVALUE:5;
end;
hence rseq1.n <= abs(Re(seq)).n by A2;
end;
now let n;
Re(seq).n = Re(seq.n) by Def3;
then A7: abs(Re(seq)).n = abs(Re(seq.n)) by SEQ_1:16;
A8: abs(Re(seq.n)) <= |.seq.n.| by Th13;
|.seq.n.| <= rseq.n by A1;
hence abs(Re(seq)).n <= rseq.n by A7,A8,AXIOMS:22;
end;
hence thesis by A6;
end;
A9: (for n holds rseq1.n <= abs(Im(seq)).n )
& (for n holds abs(Im(seq)).n <= rseq.n)
proof
A10:
now let n;
0 <= abs(Im(seq)).n
proof
abs(Im(seq)).n=abs(Im(seq).n) by SEQ_1:16;
hence thesis by ABSVALUE:5;
end;
hence rseq1.n <= abs(Im(seq)).n by A2;
end;
now let n;
A11: Im(seq).n = Im(seq.n) by Def4;
A12: abs(Im(seq)).n = abs(Im(seq).n) by SEQ_1:16;
A13: abs(Im(seq.n)) <= |.seq.n.| by Th13;
|.seq.n.| <= rseq.n by A1;
hence abs(Im(seq)).n <= rseq.n by A11,A12,A13,AXIOMS:22;
end;
hence thesis by A10;
end;
A14: abs(Re(seq)) is convergent by A1,A4,A5,SEQ_2:33;
A15: lim(abs(Re(seq)))=0 by A1,A4,A5,SEQ_2:34;
A16:abs(Im(seq)) is convergent by A1,A4,A9,SEQ_2:33;
A17:lim(abs(Im(seq)))=0 by A1,A4,A9,SEQ_2:34;
A18: Re(seq) is convergent & lim(Re(seq))=0 by A14,A15,SEQ_4:28;
Im(seq) is convergent & lim(Im(seq))=0 by A16,A17,SEQ_4:28;
then seq is convergent & Re lim(seq)=0 &Im lim(seq)=0 by A18,Th42;
hence thesis by COMPLEX1:8,L0;
end;
begin :: Summable and Absolutely Summable Complex Sequences
definition let seq, seq1 be Complex_Sequence;
pred seq is_subsequence_of seq1 means :Def9:
ex Nseq st seq = seq1(#)Nseq;
end;
theorem
seq is_subsequence_of seq1 implies
Re seq is_subsequence_of Re seq1 & Im seq is_subsequence_of Im seq1
proof
assume seq is_subsequence_of seq1; then consider Nseq such that
A1:seq=seq1(#)Nseq by Def9;
Re seq=Re seq1* Nseq by A1,Th22;
hence Re seq is_subsequence_of Re seq1 by SEQM_3:def 10;
Im seq=Im seq1 * Nseq by A1,Th22;
hence thesis by SEQM_3:def 10;
end;
theorem Th50:
seq is_subsequence_of seq1 & seq1 is_subsequence_of seq2
implies seq is_subsequence_of seq2
proof
assume that
A1: seq is_subsequence_of seq1 and
A2: seq1 is_subsequence_of seq2;
consider Nseq such that
A3: seq=seq1(#)Nseq by A1,Def9;
consider Nseq1 such that
A4: seq1=seq2(#)Nseq1 by A2,Def9;
now let n;
thus (seq2(#)(Nseq1 * Nseq)).n = seq2.((Nseq1 * Nseq).n) by Def5
.=seq2.(Nseq1.(Nseq.n)) by SEQM_3:31
.=(seq2(#)Nseq1).(Nseq.n) by Def5
.=seq.n by A3,A4,Def5;
end;
then seq=seq2(#)(Nseq1*Nseq) by COMSEQ_1:6;
hence seq is_subsequence_of seq2 by Def9;
end;
theorem
seq is bounded implies
ex seq1 st seq1 is_subsequence_of seq & seq1 is convergent
proof
assume seq is bounded;
then consider r being Real such that
A1: 0 < r & for n holds |.seq.n.| <r by COMSEQ_2:8;
now let n;
A2: |.seq.n.| <r by A1;
A3:abs (Re seq.n)=abs(Re(seq.n)) by Def3;
abs(Re(seq.n)) <= |.seq.n.| by Th13;
hence abs(Re seq.n) < r by A2,A3,AXIOMS:22;
end;
then Re seq is bounded by A1,SEQ_2:15;
then consider rseq1 such that
A4: rseq1 is_subsequence_of Re seq
& rseq1 is convergent by SEQ_4:57;
consider Nseq such that
A5: rseq1=Re seq*Nseq by A4,SEQM_3:def 10;
A6:
now let n;
|. (seq (#) Nseq).n .|=|. seq.(Nseq.n) .| by Def5;
hence |. (seq (#) Nseq).n .| < r by A1;
end;
now let n;
A7: |.(seq(#) Nseq).n.| <r by A6;
A8:abs(Im (seq(#)Nseq).n)=abs(Im((seq(#) Nseq).n)) by Def4;
abs(Im((seq(#) Nseq).n)) <= |.(seq(#) Nseq).n.| by Th13;
hence abs(Im (seq(#)Nseq).n) < r by A7,A8,AXIOMS:22;
end;
then Im (seq(#)Nseq) is bounded by A1,SEQ_2:15;
then consider rseq2 such that
A9: rseq2 is_subsequence_of Im (seq(#)Nseq)
& rseq2 is convergent by SEQ_4:57;
consider Nseq1 such that
A10: rseq2=Im (seq(#)Nseq)*Nseq1 by A9,SEQM_3:def 10;
A11: seq(#)Nseq is_subsequence_of seq by Def9;
(seq(#)Nseq)(#)Nseq1 is_subsequence_of seq(#)Nseq by Def9;
then A12: (seq(#)Nseq)(#)Nseq1 is_subsequence_of seq by A11,Th50;
A13: Im ((seq(#)Nseq)(#)Nseq1) is convergent by A9,A10,Th22;
Re ((seq(#)Nseq)(#)Nseq1)=(Re (seq(#)Nseq))*Nseq1 by Th22
.=rseq1*Nseq1 by A5,Th22;
then Re ((seq(#)Nseq)(#)
Nseq1) is_subsequence_of rseq1 by SEQM_3:def 10;
then Re ((seq(#)Nseq)(#)Nseq1) is convergent by A4,SEQ_4:29;
then (seq(#)Nseq)(#)Nseq1 is convergent by A13,Th42;
hence thesis by A12;
end;
definition let seq be Complex_Sequence;
attr seq is summable means :Def10:
Partial_Sums seq is convergent;
end;
deffunc z(set) = 0c;
definition
cluster summable Complex_Sequence;
existence
proof
consider C being Complex_Sequence such that
A1: for n holds C.n = z(n) from ExComplexSeq;
take C;
take 0c;
let p be Real such that
A2: 0<p;
take 0;
let m such that 0<=m;
thus |.Partial_Sums C.m-0c.|<p by A1,A2,Th24,COMPLEX1:130;
end;
end;
definition let seq be summable Complex_Sequence;
cluster Partial_Sums seq -> convergent;
coherence by Def10;
end;
definition let seq;
attr seq is absolutely_summable means :Def11:
|.seq.| is summable;
end;
theorem Th52:
(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 number such that
A2: 0<p;
take 0;
let m such that 0<=m;
abs((Partial_Sums |.seq.|).m-0) = abs(0-0) by A1,Th25
.= 0 by ABSVALUE:def 1;
hence abs((Partial_Sums |.seq.|).m-0)<p by A2;
end;
definition
cluster absolutely_summable Complex_Sequence;
existence
proof
consider C being Complex_Sequence such that
A1: for n holds C.n = z(n) from ExComplexSeq;
take C;
thus thesis by A1,Th52;
end;
end;
definition let seq be absolutely_summable Complex_Sequence;
cluster |.seq.| -> summable;
coherence by Def11;
end;
theorem Th53:
seq is summable implies seq is convergent & lim seq = 0c
proof
assume seq is summable;
then Partial_Sums(seq) is convergent by Def10;
then Re Partial_Sums(seq) is convergent
&Im Partial_Sums(seq) is convergent by Th41;
then Partial_Sums(Re seq) is convergent
&Partial_Sums(Im seq) is convergent by Th26;
then Re seq is summable & Im seq is summable by SERIES_1:def 2;
then Re seq is convergent & lim(Re seq)=0
& Im seq is convergent & lim(Im seq)=0 by SERIES_1:7;
then seq is convergent & Re(lim(seq))=0 &Im(lim(seq))=0 by Th42;
hence thesis by COMPLEX1:8,L0;
end;
definition
cluster summable -> convergent Complex_Sequence;
coherence by Th53;
end;
theorem Th54:
seq is summable implies
Re seq is summable & Im seq is summable
& Sum(seq)=[*Sum(Re seq),Sum(Im seq)*]
proof
assume seq is summable;
then A1: Partial_Sums(seq) is convergent by Def10;
then Re Partial_Sums(seq) is convergent
&Im Partial_Sums(seq) is convergent by Th41;
then A2: Partial_Sums(Re seq) is convergent
&Partial_Sums(Im seq) is convergent by Th26;
A3:lim(Re Partial_Sums(seq))=lim(Partial_Sums(Re seq)) &
lim(Im Partial_Sums(seq))=lim(Partial_Sums(Im seq)) by Th26;
A4:lim(Partial_Sums(Re seq))=Sum(Re seq) &
lim(Partial_Sums(Im seq))=Sum(Im seq) by SERIES_1:def 3;
lim(Re Partial_Sums(seq))=Re(lim(Partial_Sums(seq))) &
lim(Im Partial_Sums(seq))=Im(lim(Partial_Sums(seq))) by A1,Th41;
then Re(Sum(seq))=lim(Re Partial_Sums(seq)) &
Im(Sum(seq))=lim(Im Partial_Sums(seq)) by Def8;
hence thesis by A2,A3,A4,COMPLEX1:8,SERIES_1:def 2;
end;
definition let seq be summable Complex_Sequence;
cluster Re seq -> summable;
coherence by Th54;
cluster Im seq -> summable;
coherence by Th54;
end;
theorem Th55:
seq1 is summable & seq2 is summable
implies
seq1+seq2 is summable & Sum(seq1+seq2)= Sum(seq1)+Sum(seq2)
proof
assume seq1 is summable & seq2 is summable;
then A1:Partial_Sums(seq1) is convergent &
Partial_Sums(seq2) is convergent by Def10;
then A2:Partial_Sums(seq1)+Partial_Sums(seq2) is
convergent by COMSEQ_2:13;
A3:Partial_Sums(seq1)+Partial_Sums(seq2)
=Partial_Sums(seq1+seq2) by Th27;
Sum(seq1+seq2)=lim(Partial_Sums(seq1+seq2)) by Def8
.=lim(Partial_Sums(seq1)+Partial_Sums(seq2)) by Th27
.=lim(Partial_Sums(seq1))+lim(Partial_Sums(seq2))
by A1,COMSEQ_2:14;
then Sum(seq1+seq2)=Sum(seq1)+lim(Partial_Sums(seq2)) by Def8
.= Sum(seq1)+Sum(seq2) by Def8;
hence thesis by A2,A3,Def10;
end;
theorem Th56:
seq1 is summable & seq2 is summable
implies
seq1-seq2 is summable & Sum(seq1-seq2)= Sum(seq1)-Sum(seq2)
proof
assume seq1 is summable & seq2 is summable;
then A1:Partial_Sums(seq1) is convergent &
Partial_Sums(seq2) is convergent by Def10;
then A2:Partial_Sums(seq1)-Partial_Sums(seq2) is
convergent by COMSEQ_2:25;
A3:Partial_Sums(seq1)-Partial_Sums(seq2)
=Partial_Sums(seq1-seq2) by Th28;
Sum(seq1-seq2)=lim(Partial_Sums(seq1-seq2)) by Def8
.=lim(Partial_Sums(seq1)-Partial_Sums(seq2)) by Th28
.=lim(Partial_Sums(seq1))-lim(Partial_Sums(seq2))
by A1,COMSEQ_2:26;
then Sum(seq1-seq2)=Sum(seq1)-lim(Partial_Sums(seq2)) by Def8
.= Sum(seq1)-Sum(seq2) by Def8;
hence thesis by A2,A3,Def10;
end;
definition let seq1, seq2 be summable Complex_Sequence;
cluster seq1 + seq2 -> summable;
coherence by Th55;
cluster seq1 - seq2 -> summable;
coherence by Th56;
end;
theorem Th57:
seq is summable implies z (#) seq is summable & Sum(z (#) seq)= z * Sum(seq)
proof
assume seq is summable;
then A1:Partial_Sums(seq) is convergent by Def10;
then A2:(z (#) Partial_Sums(seq)) is convergent by COMSEQ_2:17;
A3:Partial_Sums(z (#) seq)=(z (#) Partial_Sums(seq)) by Th29;
Sum(z (#) seq)=lim(Partial_Sums(z (#) seq)) by Def8
.=lim((z (#) Partial_Sums(seq))) by Th29
.=z * lim(Partial_Sums(seq)) by A1,COMSEQ_2:18
.=z * Sum(seq) by Def8;
hence z (#) seq is summable
& Sum(z (#) seq)= z * Sum(seq) by A2,A3,Def10;
end;
definition let z be Element of COMPLEX,
seq be summable Complex_Sequence;
cluster z (#) seq -> summable;
coherence by Th57;
end;
theorem Th58:
Re seq is summable & Im seq is summable implies
seq is summable & Sum(seq)=[*Sum(Re seq),Sum(Im seq)*]
proof
assume
Re seq is summable & Im seq is summable;
then Partial_Sums(Re seq) is convergent
&Partial_Sums(Im seq) is convergent
by SERIES_1:def 2;
then A1: Re Partial_Sums(seq) is convergent
&Im Partial_Sums(seq) is convergent by Th26;
then A2: Partial_Sums(seq) is convergent by Th42;
A3:lim(Re Partial_Sums(seq))=lim(Partial_Sums(Re seq)) &
lim(Im Partial_Sums(seq))=lim(Partial_Sums(Im seq)) by Th26;
A4:lim(Partial_Sums(Re seq))=Sum(Re seq) &
lim(Partial_Sums(Im seq))=Sum(Im seq) by SERIES_1:def 3;
lim(Re Partial_Sums(seq))=Re(lim(Partial_Sums(seq))) &
lim(Im Partial_Sums(seq))=Im(lim(Partial_Sums(seq))) by A1,Th42;
then Re(Sum(seq))=lim(Re Partial_Sums(seq)) &
Im(Sum(seq))=lim(Im Partial_Sums(seq)) by Def8;
hence thesis by A2,A3,A4,Def10,COMPLEX1:8;
end;
theorem Th59:
seq is summable implies for n holds seq^\n is summable
proof
assume
A1: seq is summable;
now let n;
Re seq is summable & Im seq is summable by A1,Th54;
then A2: Re seq^\n is summable & Im seq^\n is summable by SERIES_1:15;
Re (seq^\n)=Re seq^\n & Im(seq^\n)=Im seq^\n by Th23;
hence seq^\n is summable by A2,Th58;
end;
hence thesis;
end;
definition let seq be summable Complex_Sequence,
n be Nat;
cluster seq^\n -> summable;
coherence by Th59;
end;
theorem
(ex n st seq^\n is summable) implies seq is summable
proof
given n such that
A1:seq^\n is summable;
A2: Re (seq^\n) is summable & Im (seq^\n) is summable by A1,Th54;
Re (seq^\n)=Re seq^\n & Im (seq^\n)=Im seq^\n by Th23;
then Re seq is summable & Im seq is summable by A2,SERIES_1:16;
hence thesis by Th58;
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 A2:Re(seq) is summable & Im(seq) is summable by Th54;
let n;
A3:seq^\(n+1) is summable by A1,Th59;
Sum(seq)=[* Sum(Re(seq)),Sum(Im(seq))*] by A1,Th54;
then A4:Re(Sum(seq))=Sum(Re(seq)) & Im(Sum(seq))=Sum(Im(seq))
by COMPLEX1:7;
A5:Sum(seq^\(n+1))=[*Sum(Re(seq^\(n+1))),Sum(Im(seq^\(n+1)))*]
by A3,Th54;
A6:Sum(Re(seq))
=Partial_Sums(Re(seq)).n + Sum(Re(seq)^\(n+1)) by A2,SERIES_1:18
.=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 A5,COMPLEX1:7
.=Re(Partial_Sums(seq).n) + Re(Sum(seq^\(n+1))) by Def3
.=Re(Partial_Sums(seq).n+ Sum(seq^\(n+1))) by COMPLEX1:19;
Sum(Im(seq))
=Partial_Sums(Im(seq)).n + Sum(Im(seq)^\(n+1)) by A2,SERIES_1:18
.=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 A5,COMPLEX1:7
.=Im(Partial_Sums(seq).n) + Im(Sum(seq^\(n+1))) by Def4
.=Im(Partial_Sums(seq).n+ Sum(seq^\(n+1))) by COMPLEX1:19;
hence Sum(seq)=Partial_Sums(seq).n+ Sum
(seq^\(n+1)) by A4,A6,COMPLEX1:def 5;
end;
theorem Th62:
Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable
proof
for n holds 0 <= |.seq.|.n by Lm1;
then Partial_Sums(|.seq.|) is bounded_above
iff |.seq.| is summable by SERIES_1:20;
hence thesis by Def11;
end;
definition let seq be absolutely_summable Complex_Sequence;
cluster Partial_Sums |.seq.| -> bounded_above;
coherence by Th62;
end;
theorem Th63:
seq is summable iff (for p st 0<p holds ex n st
for m st n <= m holds |.Partial_Sums(seq).m-Partial_Sums(seq).n.|<p)
proof
A1:now assume
seq is summable;
then Partial_Sums(seq) is convergent by Def10;
hence
for p st 0<p holds ex n st for m st n <= m
holds |.Partial_Sums(seq).m-Partial_Sums(seq).n.|<p by Th46;
end;
now assume for p st 0<p holds ex n st for m st n <= m
holds |.Partial_Sums(seq).m-Partial_Sums(seq).n.|< p;
then Partial_Sums(seq) is convergent by Th46;
hence seq is summable by Def10;
end;
hence thesis by A1;
end;
theorem Th64:
seq is absolutely_summable implies seq is summable
proof
assume seq is absolutely_summable;
then |.seq.| is summable by Def11;
then A1: Partial_Sums(|.seq.|) is convergent by SERIES_1:def 2;
now let p;
assume 0<p;
then consider n such that
A2: for m st n <= m holds
abs(Partial_Sums(|.seq.|).m-Partial_Sums(|.seq.|).n)< p by A1,SEQ_4:58;
take n;
let m; assume n <= m;
then A3: abs(Partial_Sums(|.seq.|).m-Partial_Sums(|.seq.|).n)< p by A2;
|.Partial_Sums(seq).m-Partial_Sums(seq).n.|
<= abs(Partial_Sums(|.seq.|).m-Partial_Sums(|.seq.|).n) by Th31;
hence
|.Partial_Sums(seq).m-Partial_Sums(seq).n.| <p by A3,AXIOMS:22;
end;
hence seq is summable by Th63;
end;
definition
cluster absolutely_summable -> summable Complex_Sequence;
coherence by Th64;
end;
definition
cluster absolutely_summable Complex_Sequence;
existence
proof
consider C being absolutely_summable Complex_Sequence;
take C;
thus thesis;
end;
end;
theorem Th65:
|.z.| < 1 implies z GeoSeq is summable & Sum(z GeoSeq) = 1r/(1r-z)
proof
assume
A1: |.z.|<1;
1r-z <>0c
proof
assume
A2: 1r-z = 0c;
0 <= abs(|.1r.|-|.z.|) by ABSVALUE:5;
then abs(|.1r.|-|.z.|)=0 by A2,COMPLEX1:130,150;
then |.1r.|-|.z.| =0 by ABSVALUE:7;
hence contradiction by A1,COMPLEX1:134,XCMPLX_1:15;
end;
then A3: 1r <> z by XCMPLX_1:14;
deffunc f(Nat) = z #N ($1+1);
consider seq1 such that
A4:for n holds seq1.n=f(n) from ExComplexSeq;
A5:seq1 is convergent & lim(seq1)=0c by A1,A4,Th44;
deffunc j(set) = 1r;
consider seq2 such that
A6:for n holds seq2.n=j(n) from ExComplexSeq;
A7:
seq2 is convergent by A6,COMSEQ_2:9;
then A8: seq2-seq1 is convergent by A5,COMSEQ_2:25;
A9: lim(seq2-seq1)=lim(seq2)-lim(seq1) by A5,A7,COMSEQ_2:26
.=1r -0c by A5,A6,COMSEQ_2:10
.=1r by COMPLEX1:52;
A10:(1r/(1r-z))(#)(seq2-seq1) is convergent by A8,COMSEQ_2:17;
A11:lim((1r/(1r-z))(#)(seq2-seq1))=1r/(1r-z) * 1r by A8,A9,COMSEQ_2:18
.=1r/(1r-z) by COMPLEX1:29;
A12:
now let n;
thus
Partial_Sums(z GeoSeq).n
= (1r - z #N (n+1))/(1r-z) by A3,Th36
.= (1r - seq1.n)/(1r-z) by A4
.= (seq2.n-seq1.n)/(1r-z) by A6
.= 1r * (seq2.n-seq1.n)/(1r-z) by COMPLEX1:29
.= (seq2.n-seq1.n) * (1r/(1r-z)) by XCMPLX_1:75
.= (1r/(1r-z)) * (seq2.n+-seq1.n) by XCMPLX_0:def 8
.= (1r/(1r-z)) * (seq2.n+(-seq1).n) by COMSEQ_1:def 9
.= (1r/(1r-z)) * (seq2+(-seq1)).n by COMSEQ_1:def 4
.= (1r/(1r-z)) * (seq2-seq1).n by COMSEQ_1:def 10
.= ((1r/(1r-z))(#)(seq2-seq1)).n by COMSEQ_1:def 7;
end;
hence Partial_Sums(z GeoSeq) is convergent by A10,COMSEQ_1:6;
lim(Partial_Sums(z GeoSeq) ) =1r/(1r-z) by A11,A12,COMSEQ_1:6;
hence Sum(z GeoSeq) = 1r/(1r-z) by Def8;
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
A1:|.z.|< 1 & (for n holds seq.(n+1) = z * seq.n);
1r-z <>0c
proof
assume
A2: 1r-z = 0c;
0 <= abs(|.1r.|-|.z.|) by ABSVALUE:5;
then abs(|.1r.|-|.z.|)=0 by A2,COMPLEX1:130,150;
then |.1r.|-|.z.| =0 by ABSVALUE:7;
hence contradiction by A1,COMPLEX1:134,XCMPLX_1:15;
end;
then A3: z <> 1r by XCMPLX_1:14;
now let n;
thus
Partial_Sums(seq).n = seq.0 * ((1r - z #N (n+1))/(1r-z)) by A1,A3,Th37
.=seq.0 * Partial_Sums(z GeoSeq).n by A3,Th36
.=(seq.0 (#) Partial_Sums(z GeoSeq)).n by COMSEQ_1:def 7;
end;
then A4: Partial_Sums(seq)=(seq.0 (#) Partial_Sums(z GeoSeq)) by COMSEQ_1:6;
z GeoSeq is summable & Sum(z GeoSeq) = 1r/(1r-z) by A1,Th65;
then A5: Partial_Sums(z GeoSeq) is convergent
& Sum(z GeoSeq) = lim(Partial_Sums(z GeoSeq)) by Def8,Def10;
then Partial_Sums(seq) is convergent
& lim(Partial_Sums(seq)) =seq.0 * lim(Partial_Sums(z GeoSeq))
by A4,COMSEQ_2:17,18;
hence
seq is summable by Def10;
Sum(seq)=lim(Partial_Sums(seq)) by Def8
.=seq.0 * Sum(z GeoSeq) by A4,A5,COMSEQ_2:18
.=seq.0 * (1r/(1r-z)) by A1,Th65
.=seq.0 * 1r/(1r-z) by XCMPLX_1:75
.=seq.0/(1r-z) by COMPLEX1:29;
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
A1:rseq1 is summable & (ex m st for n st m<=n holds |.seq2.n.| <= rseq1.n );
then consider m such that
A2: for n st m<=n holds |.seq2.n.| <= rseq1.n;
A3:now let n; assume
m <= n;
then |.seq2.n.| <= rseq1.n by A2;
hence |.seq2.|.n <= rseq1.n by COMSEQ_1:def 14;
end;
now
let n;
|.seq2.n.|=|.seq2.|.n by COMSEQ_1:def 14;
hence 0 <= |.seq2.|.n by COMPLEX1:132;
end;
hence |.seq2.| is summable by A1,A3,SERIES_1:22;
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.|
proof
assume A1:
(for n holds 0 <= |.seq1.|.n & |.seq1.|.n <= |.seq2.|.n)
& seq2 is absolutely_summable;
then |.seq2.| is summable by Def11;
hence |.seq1.| is summable & Sum(|.seq1.|)<=Sum(|.seq2.|) by A1,SERIES_1:24;
end;
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
proof
assume
(for n holds |.seq.|.n>0) & (ex m st for n st n>=m holds |.seq.|.(n+1)/
|.seq.|.n >= 1);
hence |.seq.| is not summable by SERIES_1:31;
end;
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 Lm1;
hence |.seq.| is summable by A1,SERIES_1:32;
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 Lm1;
hence |.seq.| is not summable by A1,SERIES_1:33;
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 Lm1;
hence |.seq.| is not summable by A1,SERIES_1:34;
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 Lm1;
then |.seq.| is summable iff rseq1 is summable by SERIES_1:35;
hence seq is absolutely_summable iff rseq1 is summable by Def11;
end;
theorem
p>1 & (for n st n>=1 holds |.seq.|.n = 1/n to_power p)
implies seq is absolutely_summable
proof
assume
p>1 & (for n st n>=1 holds |.seq.|.n = 1/n to_power p);
then |.seq.| is summable by SERIES_1:36;
hence thesis by Def11;
end;
theorem
p<=1 & (for n st n>=1 holds |.seq.|.n=1/n to_power p)
implies not seq is absolutely_summable
proof
assume p<=1 & (for n st n>=1 holds |.seq.|.n=1/n to_power p);
then not |.seq.| is summable by SERIES_1:37;
hence thesis by Def11;
end;
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
A1:(for n holds seq.n<>0c & rseq1.n=|.seq.|.(n+1)/|.seq.|.n)
&
rseq1 is convergent & lim rseq1 < 1;
now let n;
A2:seq.n<>0c & rseq1.n=|.seq.|.(n+1)/|.seq.|.n by A1;
A3:0 <= |.seq.|.n
& 0 <= |.seq.|.(n+1) by Lm1;
A4: abs((|.seq.|)).n =abs((|.seq.|).n) by SEQ_1:16
.=|.seq.|.n by A3,ABSVALUE:def 1;
A5: abs((|.seq.|)).(n+1) =abs((|.seq.|).(n+1)) by SEQ_1:16
.=|.seq.|.(n+1) by A3,ABSVALUE:def 1;
A6: |.seq.|.n =|.seq.n.| by COMSEQ_1:def 14;
hence
|.seq.|.n <>0 & rseq1.n=|.seq.|.(n+1)/|.seq.|.n by A2,COMPLEX1:133;
thus
(|.seq.|).n <>0 & rseq1.n=abs((|.seq.|)).(n+1)/|.seq.|.n
by A2,A5,A6,COMPLEX1:133;
thus (|.seq.|).n <>0 &
rseq1.n=abs((|.seq.|)).(n+1)/abs((|.seq.|)).n by A2,A4,A5,A6,COMPLEX1:133;
end;
then |.seq.| is absolutely_summable by A1,SERIES_1:42;
then A7:abs(|.seq.|) is summable by SERIES_1:def 5;
now let n;
A8:0 <= |.seq.|.n by Lm1;
thus
abs((|.seq.|)).n =abs((|.seq.|).n) by SEQ_1:16
.=|.seq.|.n by A8,ABSVALUE:def 1;
end;
then abs((|.seq.|)) = |.seq.| by FUNCT_2:113;
hence seq is absolutely_summable by A7,Def11;
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
A1: (for n holds seq.n<>0c)
& (ex m st for n st n>=m holds |.seq.|.(n+1)/|.seq.|.n >= 1);
A2:now let n;
seq.n<>0c by A1;
then |.seq.n.|<>0 by COMPLEX1:133;
hence |.seq.|.n <>0 by COMSEQ_1:def 14;
end;
consider m such that
A3:for n st n>=m holds |.seq.|.(n+1)/|.seq.|.n >= 1 by A1;
now let n such that
A4:n>=m;
A5:0 <= |.seq.|.n
& 0 <= |.seq.|.(n+1) by Lm1;
A6: abs((|.seq.|)).n =abs((|.seq.|).n) by SEQ_1:16
.=|.seq.|.n by A5,ABSVALUE:def 1;
abs((|.seq.|)).(n+1) =abs((|.seq.|).(n+1)) by SEQ_1:16
.=|.seq.|.(n+1) by A5,ABSVALUE:def 1;
hence abs((|.seq.|)).(n+1)/abs((|.seq.|)).n >= 1 by A3,A4,A6;
end;
hence |.seq.| is not summable by A2,SERIES_1:44;
end;