:: Convergence and the Limit of Complex Sequences. Series
:: by Yasunari Shidama and Artur Korni{\l}owicz
::
:: Received June 25, 1997
:: Copyright (c) 1997-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SEQ_1, COMSEQ_1, SUBSET_1, REAL_1, COMPLEX1, CARD_1,
ARYTM_3, RELAT_1, XCMPLX_0, FUNCT_1, SERIES_1, XXREAL_0, ARYTM_1,
FUNCOP_1, SEQ_2, VALUED_0, ORDINAL2, NAT_1, PREPOWER, NEWTON, SQUARE_1,
VALUED_1, CARD_3, POWER, XXREAL_2, PARTFUN1, TARSKI, FUNCT_7, ASYMPT_1,
XREAL_0;
notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0,
COMPLEX1, REAL_1, NEWTON, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1,
VALUED_1, SEQ_1, SEQ_2, NAT_1, VALUED_0, SERIES_1, SQUARE_1, POWER,
COMSEQ_1, COMSEQ_2;
constructors XREAL_0, PARTFUN1, FUNCT_3, FUNCOP_1, ARYTM_0, REAL_1, SQUARE_1,
NAT_1, SEQM_3, COMSEQ_2, NEWTON, SERIES_1, RECDEF_1, SEQ_2, VALUED_1,
SEQ_4, RELSET_1, BINOP_2, RVSUM_1, SEQ_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, NAT_1, MEMBERED, COMSEQ_2, NEWTON, VALUED_0, VALUED_1,
SEQ_4, SERIES_1, SQUARE_1, SEQ_1, SEQ_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions COMSEQ_2, SERIES_1, VALUED_0;
equalities SERIES_1, SQUARE_1, VALUED_1;
expansions COMSEQ_2, SERIES_1, FUNCT_2;
theorems NAT_1, ABSVALUE, SEQ_1, SEQ_2, SERIES_1, SEQM_3, SEQ_4, POWER,
COMPLEX1, COMSEQ_2, SQUARE_1, FUNCT_2, XCMPLX_0, XCMPLX_1, FUNCOP_1,
XREAL_1, NEWTON, XXREAL_0, ORDINAL1, VALUED_0, VALUED_1, FUNCT_1,
RELAT_1, RELSET_1, PARTFUN1;
schemes NAT_1, SEQ_1, COMSEQ_1, FUNCT_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;
Lm1: 0c = 0+0*<i>;
theorem
n+1 <> 0c & (n+1)*<i> <> 0c;
theorem Th2:
(for n holds rseq.n = 0) implies for m holds (Partial_Sums abs( rseq)).m = 0
proof
defpred P[Nat] means
abs(rseq).$1 = (Partial_Sums abs(rseq)).$1;
assume
A1: for n holds rseq.n = 0;
A2: for k st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
thus abs(rseq).(k+1) = 0 + abs(rseq).(k+1)
.= |.0.| + abs(rseq).(k+1) by ABSVALUE:def 1
.= |.rseq.k.| + abs(rseq).(k+1) by A1
.= (Partial_Sums abs(rseq)).k + abs(rseq).(k+1) by A3,SEQ_1:12
.= (Partial_Sums abs(rseq)).(k+1) by SERIES_1:def 1;
end;
let m;
A4: P[0] by SERIES_1:def 1;
for n holds P[n] from NAT_1:sch 2(A4,A2);
hence (Partial_Sums abs(rseq)).m = abs(rseq).m .= |.rseq.m.| by SEQ_1:12
.= |.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 such that
A2: 0<p;
take 0;
let m be Nat such that
0<=m;
|.(Partial_Sums abs(rseq)).m-0.| = |.0-0.| by A1,Th2
.= 0 by ABSVALUE:def 1;
hence |.(Partial_Sums abs(rseq)).m-0.|<p by A2;
end;
set C = seq_const 0;
Lm2: for n being Nat holds C.n = 0;
registration
cluster summable -> 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<p ex n st
for m,l be Nat st n <= m & n <= l holds |.rseq.m-rseq.l.|<p
proof
assume
A1: rseq is convergent;
let p;
assume 0<p;
then consider n such that
A2: for m st n <= m holds |.rseq.m-rseq.n.|<p/2 by A1,SEQ_4:41;
take n;
now
let m,l be Nat;
assume n <= m & n <= l;
then |.rseq.m-rseq.n.|<p/2 & |.rseq.l-rseq.n.|<p/2 by A2;
then
A3: |.rseq.m-rseq.n.|+|.rseq.l-rseq.n.| < p/2+p/2 by XREAL_1:8;
|.rseq.m-rseq.l.| = |.(rseq.m-rseq.n)-(rseq.l-rseq.n).|;
then |.rseq.m-rseq.l.| <= |.rseq.m-rseq.n.|+|.rseq.l-rseq.n.| by
COMPLEX1:57;
hence |.rseq.m-rseq.l.| < p by A3,XXREAL_0:2;
end;
hence thesis;
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;
let n;
defpred P[Nat] means
Partial_Sums(rseq).(n+$1)-Partial_Sums(rseq).n <= p * $1;
A2: now
let l be Nat such that
A3: P[l];
rseq.(n+l+1) <= p by A1;
then
A4: p * l + rseq.(n+l+1) <= p * l + p by XREAL_1:6;
Partial_Sums(rseq).(n+(l+1))-Partial_Sums(rseq).n =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);
then
Partial_Sums(rseq).(n+(l+1))-Partial_Sums(rseq).n <= p * l + rseq.(n
+l+1) by A3,XREAL_1:6;
hence P[l+1] by A4,XXREAL_0:2;
end;
A5: P[0];
thus for l be Nat holds P[l] from NAT_1:sch 2(A5,A2);
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;
A2: now
let n be Nat such that
A3: P[n];
rseq.(n+1) <= p by A1;
then
A4: p * (n+1)+ rseq.(n+1) <= p * (n+1) + p by XREAL_1:6;
Partial_Sums(rseq).(n+1) =Partial_Sums(rseq).(n)+rseq.(n+1) by
SERIES_1:def 1;
then Partial_Sums(rseq).(n+1) <= p * (n+1) + rseq.(n+1) by A3,XREAL_1:6;
hence P[n+1] by A4,XXREAL_0:2;
end;
Partial_Sums(rseq).(0) =rseq.0 by SERIES_1:def 1;
then
A5: P[0] by A1;
thus for n be Nat holds P[n] from NAT_1:sch 2(A5,A2);
end;
theorem
(for n st n <= m holds rseq1.n <= p * rseq2.n) implies Partial_Sums(
rseq1).m <= p * Partial_Sums(rseq2).m
proof
defpred P[Nat] means
$1 <= m implies Partial_Sums(rseq1).$1 <= p
* Partial_Sums(rseq2).$1;
assume
A1: for n st n <= m holds rseq1.n <= p * rseq2.n;
A2: now
let n be Nat such that
A3: P[n];
now
assume
A4: n + 1 <= m;
then rseq1.(n+1) <= p * rseq2.(n+1) by A1;
then
A5: p * Partial_Sums(rseq2).(n) + rseq1.(n+1) <= p * Partial_Sums(rseq2
).(n) + p * rseq2.(n+1) by XREAL_1:6;
n < n+1 & Partial_Sums(rseq1).(n+1) =Partial_Sums(rseq1).(n)+rseq1.
(n+1) by SERIES_1:def 1,XREAL_1:29;
then
A6: Partial_Sums(rseq1).(n+1) <= p * Partial_Sums(rseq2).(n) + rseq1.(n
+1) by A3,A4,XREAL_1:6,XXREAL_0:2;
p * Partial_Sums(rseq2).(n) + p * rseq2.(n+1) =p * (Partial_Sums(
rseq2).(n) +rseq2.(n+1))
.=p * Partial_Sums(rseq2).(n+1) by SERIES_1:def 1;
hence Partial_Sums(rseq1).(n+1) <= p * Partial_Sums(rseq2).(n+1) by A6,A5
,XXREAL_0:2;
end;
hence P[n+1];
end;
A7: P[0]
proof
assume 0 <= m;
Partial_Sums(rseq1).(0) =rseq1.0 & p * Partial_Sums(rseq2).(0) =p *
rseq2.0 by SERIES_1:def 1;
hence thesis by A1;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A7,A2);
hence thesis;
end;
theorem
(for n st n <= m holds rseq1.n <= p * rseq2.n) implies for n 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;
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: for l be Nat st P[l] holds P[l+1]
proof
let l be Nat such that
A3: P[l];
assume
A4: n + (l+1) <= m;
then
Partial_Sums(rseq1).(n+(l+1)) =Partial_Sums(rseq1).(n+l)+rseq1.(n+l+1)
& rseq1.(n+l+1) <= p * rseq2.(n+l+1) by A1,SERIES_1:def 1;
then Partial_Sums(rseq1).(n+(l+1)) <= Partial_Sums(rseq1).(n+l) + p *
rseq2.(n+l+1) by XREAL_1:6;
then
A5: 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 XREAL_1:9;
n+l < (n+l)+1 by XREAL_1:29;
then
A6: 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 A3,A4,XREAL_1:6,XXREAL_0:2;
p * (Partial_Sums(rseq2).(n+l)-Partial_Sums(rseq2).n) + p * rseq2.(n+
l+1) = p * (Partial_Sums(rseq2).(n+l)+rseq2.(n+l+1) -Partial_Sums(rseq2).n)
.=p * (Partial_Sums(rseq2).(n+(l+1)) -Partial_Sums(rseq2).n) by
SERIES_1:def 1;
hence thesis by A5,A6,XXREAL_0:2;
end;
A7: P[0];
thus for l be Nat holds P[l] from NAT_1:sch 2(A7,A2);
end;
theorem
(for n holds 0 <= rseq.n) implies (for n, m st n <= m holds |.
Partial_Sums(rseq).m-Partial_Sums(rseq).n.| =Partial_Sums(rseq).m-Partial_Sums(
rseq).n) & for n holds |.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:16;
A3: now
let n,m;
assume n <= m;
then Partial_Sums(rseq).n <= Partial_Sums(rseq).m by A2,SEQM_3:6;
then Partial_Sums(rseq).n-Partial_Sums(rseq).n <= Partial_Sums(rseq).m-
Partial_Sums(rseq).n by XREAL_1:9;
hence
|.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 <= Partial_Sums(rseq).n by A2,SEQM_3:6;
Partial_Sums(rseq).0 = rseq.0 & 0 <= rseq.0 by A1,SERIES_1:def 1;
hence |.Partial_Sums(rseq).n.|=Partial_Sums(rseq).n by A4,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 that
A1: seq1 is convergent & seq2 is convergent and
A2: lim(seq1-seq2)=0c;
lim(seq1-seq2)=lim(seq1)-lim(seq2) by A1,COMSEQ_2:26;
hence thesis by A2;
end;
begin :: The Operations on Complex Sequences
reserve z for Complex;
reserve Nseq,Nseq1 for increasing sequence of NAT;
Lm3: |.seq.n.|=|.seq.|.n & 0 <= |.seq.|.n
proof
|.seq.n.|=|.seq.|.n by VALUED_1:18;
hence thesis by COMPLEX1:46;
end;
definition
let z be Complex;
func z GeoSeq -> 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 :: redefines |^ (NEWTON, definition)
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; :: redefines Re (COMSEQ_3, definition)
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; :: redefines Im (COMSEQ_3, definition)
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 :: redefines Re (COMSEQ_3, definition)
: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 :: redefines Im (COMSEQ_3, definition)
: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)*<i> by COMPLEX1:13;
then
A1: |.z.| <= |.Re z +0*<i>.| +|.0+(Im z)*<i>.| by COMPLEX1:56;
Re(0+(Im z)*<i>)=0 & Im(0+(Im z)*<i>)=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*<i>;
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)*<i> by
COMPLEX1:82
.= r * Re z+(r * Im z)*<i> 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))*<i>) 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))*<i>) 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))*<i>) 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))*<i>) 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; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
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; :: redefines Partial_Sums (SERIES_1, definition)
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<p ex n st for m st n<=m holds |.a.m
-a1.| < p by A2,SEQ_2:def 6;
consider b1 being Real such that
A5: for p being Real st 0<p ex n st for m st n<=m holds |.b.m
-b1.|<p by A3,SEQ_2:def 6;
reconsider a1,b1 as Real;
reconsider g=a1+b1*<i> as Element of COMPLEX by XCMPLX_0:def 2;
take g;
for p st 0<p holds ex n st for m st n <= m holds |.c.m-g.|< p
proof
let p;
assume
A6: 0 < p;
then consider n1 such that
A7: for m st n1<=m holds |.a.m-a1.|< p/2 by A4;
consider n2 such that
A8: for m st n2<=m holds |.b.m-b1.|< p/2 by A5,A6;
n1 <= (n1+n2) & n2 <= (n1+n2) by NAT_1:11;
then consider n such that
A9: n1 <= n and
A10: n2 <= n;
take n;
for m st n <= m holds |.c.m-g.|< p
proof
let m;
Re(c.m)=a.m & Re g =a1 by A1,COMPLEX1:12;
then
A11: Re(c.m-g)=a.m-a1 by COMPLEX1:19;
Im(c.m)=b.m & Im g =b1 by A1,COMPLEX1:12;
then
A12: Im(c.m-g)=b.m-b1 by COMPLEX1:19;
assume
A13: n <= m;
then n2 <= m by A10,XXREAL_0:2;
then
A14: |.b.m-b1.|< p/2 by A8;
n1 <= m by A9,A13,XXREAL_0:2;
then |.a.m-a1.|< p/2 by A7;
then
A15: |.a.m-a1.| + |.b.m-b1.|< p/2+ p/2 by A14,XREAL_1:8;
|.c.m-g.| <= |.Re(c.m-g).| + |.Im(c.m-g).| by Th12;
hence thesis by A15,A11,A12,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis;
end;
assume c is convergent;
then consider z being Complex such that
A16: for p being Real st 0<p ex n st for m st n <= m holds |.c.m-z.| < p;
thus a is convergent
proof
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
take Re z;
let p be Real;
assume
A17: 0<p;
consider n such that
A18: for m st n <= m holds |.c.m-z.| < p by A16,A17;
take n;
let m;
assume n <= m;
then
A19: |.c.m-z.| < p by A18;
Re(c.m) =a.m & Re(c.m-z)=Re(c.m)-Re(z) by A1,COMPLEX1:19;
then |.a.m-Re(z).| <= |.c.m-z.| by Th13;
hence thesis by A19,XXREAL_0:2;
end;
take Im z;
let p be Real;
assume
A20: p>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)*<i>
proof
let a, b be convergent Real_Sequence, c be Complex_Sequence;
reconsider g=lim(a)+lim(b)*<i> 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<p ex n st for m st n<=m holds |.c.m-g.| < p
proof
let p be Real;
assume
A3: 0 < p;
then consider n1 such that
A4: for m st n1<=m holds |.a.m-lim(a).|< p/2 by SEQ_2:def 7;
consider n2 such that
A5: for m st n2<=m holds |.b.m-lim(b).|< p/2 by A3,SEQ_2:def 7;
n1 <= n1+n2 & n2 <= n1+n2 by NAT_1:11;
then consider n such that
A6: n1 <= n and
A7: n2 <= n;
take n;
let m;
assume
A8: n <= m;
then n2 <= m by A7,XXREAL_0:2;
then
A9: |.b.m-lim(b).|< p/2 by A5;
n1 <= m by A6,A8,XXREAL_0:2;
then |.a.m-lim(a).|< p/2 by A4;
then
A10: |.a.m-lim(a).| + |.b.m-lim(b).|< p/2+ p/2 by A9,XREAL_1:8;
Re(c.m)=a.m & Re(g) =lim(a) by A1,COMPLEX1:12;
then
A11: Re(c.m-g)=a.m-lim(a) by COMPLEX1:19;
Im(c.m)=b.m & Im(g) =lim(b) by A1,COMPLEX1:12;
then
A12: Im(c.m-g)=b.m-lim(b) by COMPLEX1:19;
|.c.m-g.| <= |.Re(c.m-g).| + |.Im(c.m-g).| by Th12;
hence thesis by A10,A11,A12,XXREAL_0:2;
end;
hence thesis by A2,COMSEQ_2:def 6;
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;
A2: for p being Real st 0<p ex n st for m st n<=m holds |.b.m-Im(
lim(c)).| <p
proof
let p be Real;
assume
A3: p>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<p ex n st for m st n<=m holds |.a.m-Re(
lim(c)).|<p
proof
let p be Real;
assume
A7: 0<p;
consider n such that
A8: for m st n <= m holds |.c.m-lim(c).| < p by A7,COMSEQ_2:def 6;
take n;
let m;
Re(c.m) =a.m by A1;
then Re(c.m-lim(c))=a.m-Re(lim(c)) by COMPLEX1:19;
then
A9: |.a.m-Re(lim(c)) .| <= |.c.m-lim(c).| by Th13;
assume n <= m;
then |.c.m-lim(c).| < p by A8;
hence thesis by A9,XXREAL_0:2;
end;
a is convergent & b is convergent by A1,Th38;
hence thesis by A6,A2,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;
( for n holds Re c.n=Re(c.n))& for n holds Im c.n=Im(c.n) by Def5,Def6;
hence thesis by Th40;
end;
registration
let c be convergent Complex_Sequence;
cluster Re c -> 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))*<i> 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<p ex n st for m st n <= m holds
|.seq.m-seq.n.|<p
proof
A1: now
assume
A2: for p st 0<p holds ex n st for m st n <= m holds |.seq.m-seq.n.|< p;
for p be Real st 0<p holds ex n st for m st n <= m holds |.
Re seq.m-Re seq.n.|<p
proof
let p be Real;
assume
A3: 0<p;
consider n such that
A4: for m st n <= m holds |.seq.m-seq.n.|<p by A2,A3;
take n;
let m;
assume n <= m;
then
A5: |.seq.m-seq.n.|<p by A4;
Re(seq.m-seq.n)=Re(seq.m)-Re(seq.n) by COMPLEX1:19
.=Re seq.m-Re(seq.n) by Def5
.=Re seq.m-Re seq.n by Def5;
then |.Re seq.m-Re seq.n.| <= |.seq.m-seq.n.| by Th13;
hence thesis by A5,XXREAL_0:2;
end;
hence
A6: Re seq is convergent by SEQ_4:41;
for p be Real st 0<p holds ex n st for m st n <= m holds |.
Im seq.m-Im seq.n.|<p
proof
let p be Real;
assume
A7: 0<p;
consider n such that
A8: for m st n <= m holds |.seq.m-seq.n.|<p by A2,A7;
take n;
let m;
assume n <= m;
then
A9: |.seq.m-seq.n.|<p by A8;
Im(seq.m-seq.n)=Im(seq.m)-Im(seq.n) by COMPLEX1:19
.=Im seq.m-Im(seq.n) by Def6
.=Im seq.m-Im seq.n by Def6;
then |.Im seq.m-Im seq.n.| <= |.seq.m-seq.n.| by Th13;
hence thesis by A9,XXREAL_0:2;
end;
hence Im seq is convergent by SEQ_4:41;
hence seq is convergent by A6,Th42;
end;
now
assume seq is convergent;
then consider z being Complex such that
A10: for p being Real st 0<p ex n st for m st n <= m holds |.seq.m-z.|<p;
let p;
assume 0< p;
then consider n such that
A11: for m st n <= m holds |.seq.m-z.|<p/2 by A10;
take n;
let m;
assume n <= m;
then
A12: |.seq.m-z.|<p/2 by A11;
|.seq.n-z.|<p/2 by A11;
then |.seq.m-z.| + |.seq.n-z.| <p/2+p/2 by A12,XREAL_1:8;
then
A13: |.seq.m-z.| + |.z-seq.n.| <p by COMPLEX1:60;
|.seq.m-seq.n.| <= |.seq.m-z.| + |.z-seq.n.| by COMPLEX1:63;
hence |.seq.m-seq.n.|< p by A13,XXREAL_0:2;
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 consider n such that
A2: for m st n <= m holds |.seq.m-seq.n.|<p/2 by A1,Th46;
take n;
let m,l be Nat;
assume n <= m & n <= l;
then |.seq.m-seq.n.|<p/2 & |.seq.l-seq.n.|<p/2 by A2;
then
A3: |.seq.m-seq.n.|+|.seq.l-seq.n.| < p/2+p/2 by XREAL_1:8;
|.(seq.m-seq.n)-(seq.l-seq.n).| <= |.seq.m-seq.n.|+|.seq.l-seq.n.| by
COMPLEX1:57;
hence |.seq.m-seq.l.| < p by A3,XXREAL_0:2;
end;
theorem
(for n holds |. seq.n .| <= rseq.n) & rseq is convergent & lim(rseq)=0
implies seq is convergent & lim(seq)=0c
proof
assume that
A1: for n holds |. seq.n .| <= rseq.n and
A2: rseq is convergent & lim(rseq)=0;
A3: 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;
C.0=0;
then
A4: lim(C)=0 by SEQ_4:25;
now
let n;
Re(seq).n = Re(seq.n) by Def5;
then
A5: abs(Re seq).n = |.Re(seq.n).| by SEQ_1:12;
|.Re(seq.n).| <= |.seq.n.| & |.seq.n.| <= rseq.n by A1,Th13;
hence abs(Re seq).n <= rseq.n by A5,XXREAL_0:2;
end;
then
A6: abs(Re seq) is convergent & lim(abs(Re seq))=0 by A2,A4,A3,SEQ_2:19,20;
then
A7: Re(seq) is convergent by SEQ_4:15;
A8: 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;
now
let n;
A9: Im(seq).n = Im(seq.n) & abs(Im seq).n = |.Im(seq).n.| by Def6,SEQ_1:12;
|.Im(seq.n).| <= |.seq.n.| & |.seq.n.| <= rseq.n by A1,Th13;
hence abs(Im seq).n <= rseq.n by A9,XXREAL_0:2;
end;
then
A10: abs(Im seq) is convergent & lim(abs(Im seq))=0 by A2,A4,A8,SEQ_2:19,20;
then
A11: Im(seq) is convergent by SEQ_4:15;
lim(Im(seq))=0 by A10,SEQ_4:15;
then
A12: Im lim(seq)=0 by A7,A11,Th42;
lim(Re(seq))=0 by A6,SEQ_4:15;
then Re lim(seq)=0 by A7,A11,Th42;
hence thesis by A7,A11,A12,Lm1,Th42,COMPLEX1:13;
end;
begin :: Summable and Absolutely Summable Complex Sequences
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 VALUED_0:def 17;
Re seq=Re seq1* Nseq by A1,Th22;
hence Re seq is subsequence of Re seq1;
Im seq=Im seq1 * Nseq by A1,Th22;
hence thesis;
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 and
A2: for n holds |.seq.n.| <r by COMSEQ_2:8;
now
let n;
|.Re seq.n.|=|.Re(seq.n).| & |.Re(seq.n).| <= |.seq.n.| by Def5,Th13;
hence |.Re seq.n.| < r by A2,XXREAL_0:2;
end;
then Re seq is bounded by A1,SEQ_2:3;
then consider rseq1 such that
A3: rseq1 is subsequence of Re seq and
A4: rseq1 is convergent by SEQ_4:40;
consider Nseq such that
A5: rseq1=Re seq*Nseq by A3,VALUED_0:def 17;
A6: now
let n;
n in NAT by ORDINAL1:def 12;
then |. (seq * Nseq).n .|=|. seq.(Nseq.n) .| by FUNCT_2:15;
hence |. (seq * Nseq).n .| < r by A2;
end;
now
let n;
|.Im (seq*Nseq).n.|=|.Im((seq* Nseq).n).| & |.Im((seq* Nseq).n).|
<= |.( seq* Nseq).n.| by Def6,Th13;
hence |.Im (seq*Nseq).n.| < r by A6,XXREAL_0:2;
end;
then Im (seq*Nseq) is bounded by A1,SEQ_2:3;
then consider rseq2 such that
A7: rseq2 is subsequence of Im (seq*Nseq) and
A8: rseq2 is convergent by SEQ_4:40;
consider Nseq1 such that
A9: rseq2=Im (seq*Nseq)*Nseq1 by A7,VALUED_0:def 17;
Re ((seq*Nseq)*Nseq1)=(Re (seq*Nseq))*Nseq1 by Th22
.=rseq1*Nseq1 by A5,Th22;
then
A10: Re ((seq*Nseq)*Nseq1) is convergent by A4,SEQ_4:16;
seq*Nseq is subsequence of seq & (seq*Nseq)*Nseq1 is subsequence of seq
*Nseq by VALUED_0:def 17;
then
A11: (seq*Nseq)*Nseq1 is subsequence of seq by VALUED_0:20;
Im ((seq*Nseq)*Nseq1) is convergent by A8,A9,Th22;
hence thesis by A11,A10,Th42;
end;
definition
let seq be Complex_Sequence;
attr seq is summable means
:Def8:
Partial_Sums seq is convergent;
end;
set D = NAT --> 0c;
registration
cluster summable for Complex_Sequence;
existence
proof
take D, 0c;
let p be Real such that
A1: 0<p;
take 0;
for n holds D.n = 0c;
hence thesis by A1,Th24,COMPLEX1:44;
end;
end;
registration
let seq be summable Complex_Sequence;
cluster Partial_Sums seq -> 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<p;
take 0;
let m;
|.(Partial_Sums |.seq.|).m-0.| = |.0-0.| by A1,Th25
.= 0 by ABSVALUE:def 1;
hence thesis by A2;
end;
registration
cluster absolutely_summable for Complex_Sequence;
existence
proof
take D;
for n holds D.n = 0c;
hence thesis by Th51;
end;
end;
registration
let seq be absolutely_summable Complex_Sequence;
cluster |.seq.| -> 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)*<i>
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)*<i>
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)))*<i> 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))))*<i> 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<p holds ex n st for m st n <= m
holds |.Partial_Sums(seq).m-Partial_Sums(seq).n.|<p by Th46;
theorem Th63:
seq is absolutely_summable implies seq is summable
proof
assume
A1: seq is absolutely_summable;
now
let p;
assume 0<p;
then consider n such that
A2: for m st n <= m holds |.Partial_Sums(|.seq.|).m-Partial_Sums(|.
seq.|).n.|< p by A1,SEQ_4:41;
take n;
let m;
assume n <= m;
then
A3: |.Partial_Sums(|.seq.|).m-Partial_Sums(|.seq.|).n.|< p by A2;
|.Partial_Sums(seq).m-Partial_Sums(seq).n.| <= |.Partial_Sums(|.seq
.|).m-Partial_Sums(|.seq.|).n.| by Th31;
hence |.Partial_Sums(seq).m-Partial_Sums(seq).n.| <p by A3,XXREAL_0:2;
end;
hence thesis by Th62;
end;
registration
cluster absolutely_summable -> 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;