:: Series
:: by Konrad Raczkowski and Andrzej N\c{e}dzusiak
::
:: Received October 15, 1990
:: Copyright (c) 1990-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, SUBSET_1, XREAL_0, ORDINAL1, SEQ_1, ARYTM_3, CARD_1,
FUNCT_1, POWER, SEQ_2, ORDINAL2, ARYTM_1, XXREAL_0, COMPLEX1, RELAT_1,
INT_1, NAT_1, REAL_1, CARD_3, VALUED_1, VALUED_0, XXREAL_2, PREPOWER,
NEWTON, SERIES_1, ABIAN, MEMBERED, XBOOLE_0, IDEAL_1, PBOOLE, TARSKI,
FUNCT_7, ASYMPT_1;
notations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1,
REAL_1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, INT_1, NAT_1,
VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, PBOOLE, FUNCT_2, NEWTON,
ABIAN, PREPOWER, POWER, FUNCOP_1, XXREAL_0;
constructors FUNCOP_1, XXREAL_0, REAL_1, NAT_1, SEQ_2, SEQM_3, NEWTON,
PREPOWER, POWER, PARTFUN1, VALUED_1, SEQ_4, RELSET_1, ABIAN, BINOP_2,
COMSEQ_2, SEQ_1, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
MEMBERED, NEWTON, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, POWER, SEQ_2,
SEQ_4, XCMPLX_0, SEQ_1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
definitions VALUED_0;
equalities VALUED_1, XCMPLX_0;
expansions VALUED_1, PBOOLE, VALUED_0;
theorems SEQ_1, SEQ_2, SEQM_3, SEQ_4, NAT_1, RFUNCT_2, ABSVALUE, INT_1,
PREPOWER, POWER, FUNCT_2, NEWTON, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0,
ORDINAL1, VALUED_0, VALUED_1, MEMBERED, XCMPLX_0, RELSET_1, PARTFUN1,
XREAL_0, TARSKI;
schemes NAT_1, SEQ_1, FUNCT_2, RECDEF_1;
begin
reserve n,m,k for Nat;
reserve a,p,r for Real;
reserve s,s1,s2,s3 for Real_Sequence;
theorem Th1:
0<a & a<1 & (for n holds s.n=a to_power (n+1)) implies
s is convergent & lim s = 0
proof
assume that
A1: 0<a and
A2: a<1 and
A3: for n holds s.n=a to_power (n+1);
set r = 1/a - 1;
1/a > 1/1 by A1,A2,XREAL_1:88;
then
A4: r > 0 by XREAL_1:50;
A5: for p be Real st 0 < p ex m st for n st m<=n holds |.s.n - 0.| < p
proof
let p be Real;
A6: 1/(p * r) <= [\1/(p * r)/] + 1 by INT_1:29;
assume
A7: 0<p;
then p * r > 0 by A4;
then 1/(p * r) > 0;
then 0 < [\1/(p * r)/] + 1;
then [\1/(p * r)/] is Element of NAT by INT_1:3,7;
then consider m such that
A8: m = [\1/(p * r)/];
take m;
A9: 1/(p * r) = 1/p/r by XCMPLX_1:78;
now
A10: [\1/(p * r)/] > 1/(p * r) -1 by INT_1:def 6;
let n;
assume m<=n;
then n > 1/(p * r) - 1 by A8,A10,XXREAL_0:2;
then n + 1 > 1/p/r by A9,XREAL_1:19;
then
A11: (n+1) * r > 1/p by A4,XREAL_1:77;
0 + (n+1) * r < 1 + (n+1) * r by XREAL_1:6;
then
A12: 1/p < 1 + (n+1) * r by A11,XXREAL_0:2;
A13: (1+r) to_power (n+1) = 1 to_power (n+1) / a to_power (n+1) by A1,POWER:31
.= 1 / a to_power (n+1);
a to_power (n+1) > 0 by A1,POWER:34;
then
A14: |.a to_power (n+1).| = a to_power (n+1) by ABSVALUE:def 1;
1 + (n+1) * r <= (1 + r) to_power (n + 1) by A4,POWER:49;
then 1/p < 1/ a to_power (n+1) by A13,A12,XXREAL_0:2;
then |.a to_power (n+1).| < p by A7,A14,XREAL_1:91;
hence |.s.n - 0.| < p by A3;
end;
hence thesis;
end;
hence s is convergent by SEQ_2:def 6;
hence thesis by A5,SEQ_2:def 7;
end;
theorem Th2:
for n being Nat holds |.a.| to_power n = |.a to_power n.|
proof
let n be Nat;
per cases;
suppose
A1: a <> 0;
then
A2: |.a.| > 0 by COMPLEX1:47;
now
per cases by A1;
suppose a>0;
then a to_power n = |.a.| to_power n & a to_power n > 0
by ABSVALUE:def 1,POWER:34;
hence thesis by ABSVALUE:def 1;
end;
suppose
A3: a < 0;
reconsider m=n as Integer;
now
per cases;
suppose
A4: m is even;
A5: |.a.| to_power n > 0 by A2,POWER:34;
|.a.| to_power n = (-a) to_power m by A3,ABSVALUE:def 1
.= a to_power m by A4,POWER:47;
hence thesis by A5,ABSVALUE:def 1;
end;
suppose
A6: m is odd;
A7: |.a.| to_power n > 0 by A2,POWER:34;
|.a.| to_power n = (-a) to_power m by A3,ABSVALUE:def 1
.= - a to_power m by A6,POWER:48;
hence |.a.| to_power n = |. - a to_power n.|
by A7,ABSVALUE:def 1
.= |. a to_power n.| by COMPLEX1:52;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A8: a = 0;
per cases;
suppose n = 0;
then a to_power n = 1 by NEWTON:4;
hence thesis by A8,COMPLEX1:44,48;
end;
suppose n > 0;
then |.a.| to_power n = 0 by A8,COMPLEX1:44,POWER:def 2;
hence thesis by A8,COMPLEX1:44;
end;
end;
end;
theorem Th3:
|.a.|<1 & (for n holds s.n=a to_power (n+1)) implies s is
convergent & lim s = 0
proof
assume that
A1: |.a.| < 1 and
A2: for n holds s.n=a to_power (n+1);
now
per cases;
suppose
|.a.| = 0;
then
A3: a = 0 by ABSVALUE:2;
now
let n be Nat;
n in NAT & a to_power (n+1) = 0 by A3,ORDINAL1:def 12,POWER:def 2;
hence s.n = In(0,REAL) by A2;
end;
then s is constant & s.0 = In(0,REAL);
hence thesis by SEQ_4:26;
end;
suppose
A4: not |.a.| = 0;
deffunc U(Nat) = |.a.| to_power ($1+1);
consider s1 such that
A5: for n holds s1.n = U(n) from SEQ_1:sch 1;
A6: now
let n;
thus s1.n = |.a.| to_power (n+1) by A5
.= |.a to_power (n+1).| by Th2
.= |.s.n.| by A2;
end;
A7: |.a.| > 0 by A4,COMPLEX1:46;
then lim s1 = 0 by A1,A5,Th1;
then
A8: lim abs(s) = 0 by A6,SEQ_1:12;
s1 is convergent by A1,A7,A5,Th1;
then abs(s) is convergent by A6,SEQ_1:12;
hence thesis by A8,SEQ_4:15;
end;
end;
hence thesis;
end;
definition
let X be non empty add-closed complex-membered set;
let s1, s2 be sequence of X;
redefine func s1+s2 -> sequence of X; :: redefines + (VALUED_1, definition)
coherence
proof
A1: dom(s1+s2) = dom s1 /\ dom s2 by VALUED_1:def 1
.= NAT /\ dom s2 by FUNCT_2:def 1
.= NAT /\ NAT by FUNCT_2:def 1;
now
let x be object such that
A2: x in NAT;
A3: s1.x in X & s2.x in X by A2,FUNCT_2:5;
(s1+s2).x = s1.x + s2.x by A1,A2,VALUED_1:def 1;
hence (s1+s2).x in X by A3,MEMBERED:def 25;
end;
hence thesis by A1,FUNCT_2:3;
end;
end;
definition
let s be complex-valued ManySortedSet of NAT;
func Partial_Sums(s) -> complex-valued ManySortedSet of NAT means
:Def1:
it.0 = s.0 & for n holds it.(n+1) = it.n + s.(n+1);
existence
proof
set X = COMPLEX;
A1: dom s = NAT by PARTFUN1:def 2;
rng s c= X;
then reconsider ss = s as sequence of X by A1,RELSET_1:4;
defpred P[Nat,Element of X,set] means $3 = $2 + ss.($1+1);
A2: for n being Nat for x being Element of X
ex y being Element of X st P[n,x,y]
proof let n be Nat, x be Element of X;
reconsider y = x + ss.(n+1) as Element of COMPLEX by XCMPLX_0:def 2;
take y;
thus thesis;
end;
consider f being sequence of X such that
A3: f.0 = ss.0 and
A4: for n being Nat holds P[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(A2);
take f;
thus f.0 = s.0 by A3;
let n;
reconsider n as Element of NAT by ORDINAL1:def 12;
P[n,f.n,f.(n+1)] by A4;
hence thesis;
end;
uniqueness
proof
let s1,s2 be complex-valued ManySortedSet of NAT;
assume that
A5: s1.0=s.0 and
A6: for n holds s1.(n+1)=s1.n + s.(n+1) and
A7: s2.0=s.0 and
A8: for n holds s2.(n+1)=s2.n + s.(n+1);
defpred X[Nat] means s1.$1 = s2.$1;
A9: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
assume s1.k =s2.k;
hence s1.(k+1) = s2.k + s.(k+1) by A6
.= s2.(k+1) by A8;
end;
A10: X[0] by A5,A7;
for n being Nat holds X[n] from NAT_1:sch 2(A10,A9);
hence thesis;
end;
end;
registration
let s be real-valued ManySortedSet of NAT;
cluster Partial_Sums s -> real-valued;
coherence
proof set f = Partial_Sums s;
let x be object;
assume
x in dom f;
then reconsider n = x as Element of NAT;
defpred P[Nat] means f.$1 is real;
f.0 = s.0 by Def1;
then
A1: P[0];
A2: for k be Nat st P[k] holds P[k + 1]
proof let k be Nat;
assume
A3: P[k];
reconsider k as Element of NAT by ORDINAL1:def 12;
f.(k+1) = f.k + s.(k+1) by Def1;
hence thesis by A3;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
then f.n is real;
hence thesis;
end;
end;
definition
let s be Real_Sequence;
redefine func Partial_Sums s -> Real_Sequence; :: redefines Partial_Sums (SERIES_1, definition)
coherence
proof
A1: dom Partial_Sums s = NAT by PARTFUN1:def 2;
rng Partial_Sums s c= REAL by VALUED_0:def 3;
then Partial_Sums s is Relation of NAT, REAL by A1,RELSET_1:4;
hence Partial_Sums s is Real_Sequence;
end;
end;
definition
let s;
attr s is summable means
:Def2:
Partial_Sums(s) is convergent;
func Sum(s) -> Real equals
lim Partial_Sums(s);
correctness;
end;
theorem Th4:
s is summable implies s is convergent & lim s = 0
proof
assume s is summable;
then
A1: Partial_Sums(s) is convergent;
now
let n;
(Partial_Sums(s)).(n+1) = (Partial_Sums(s)).n + s.(n+1) by Def1;
then (Partial_Sums(s)).(n+1) = (Partial_Sums(s)).n + (s ^\1).n by
NAT_1:def 3;
hence (Partial_Sums(s) ^\1).n = (Partial_Sums(s)).n + (s ^\1).n by
NAT_1:def 3;
end;
then
A2: (Partial_Sums(s) ^\1) = Partial_Sums(s) + s ^\1 by SEQ_1:7;
now
let n be Element of NAT;
thus (s ^\1 + (Partial_Sums(s) - Partial_Sums(s))).n = (s ^\1).n + (
Partial_Sums(s) +- Partial_Sums(s)).n by SEQ_1:7
.= (s ^\1).n + ((Partial_Sums(s)).n + (-Partial_Sums(s)).n) by SEQ_1:7
.= (s ^\1).n + ((Partial_Sums(s)).n +- (Partial_Sums(s)).n) by SEQ_1:10
.= (s ^\1).n;
end;
then s ^\1 + (Partial_Sums(s) - Partial_Sums(s)) = s ^\1;
then
A3: s ^\1 = Partial_Sums(s) ^\1 - Partial_Sums(s) by A2,SEQ_1:31;
then
A4: s ^\1 qua Real_Sequence is convergent by A1;
hence s is convergent by SEQ_4:21;
lim(Partial_Sums(s) ^\1) = lim(Partial_Sums(s)) by A1,SEQ_4:20;
then
lim(Partial_Sums(s) ^\1 - Partial_Sums(s)) = lim(Partial_Sums(s)) - lim(
Partial_Sums(s)) by A1,SEQ_2:12
.= 0;
hence thesis by A3,A4,SEQ_4:22;
end;
Lm1:
for seq,seq1,seq2 being complex-valued ManySortedSet of NAT holds
seq = seq1 + seq2 iff for n holds seq.n =seq1.n + seq2.n
proof
let seq,seq1,seq2 be complex-valued ManySortedSet of NAT;
thus seq = seq1 + seq2 implies for n holds seq.n =seq1.n + seq2.n
proof
assume
A1: seq = seq1 + seq2;
let n;
A2: n in NAT by ORDINAL1:def 12;
dom seq = NAT by PARTFUN1:def 2;
hence thesis by A1,VALUED_1:def 1,A2;
end;
assume for n holds seq.n =seq1.n + seq2.n;
then
A3: for n being object st n in dom seq holds seq.n = seq1.n + seq2.n;
dom seq = NAT /\ NAT by PARTFUN1:def 2
.= NAT /\ dom seq2 by PARTFUN1:def 2
.= dom seq1 /\ dom seq2 by PARTFUN1:def 2;
hence thesis by A3,VALUED_1:def 1;
end;
theorem Th5:
for X being non empty add-closed complex-membered set
for s1,s2 being sequence of X holds
Partial_Sums(s1) + Partial_Sums(s2) = Partial_Sums(s1+s2)
proof
let X be non empty add-closed complex-membered set;
let s1,s2 be sequence of X;
A1: now
let n;
thus (Partial_Sums(s1) + Partial_Sums(s2)).(n+1) = Partial_Sums(s1).(n+1)
+ Partial_Sums(s2).(n+1) by Lm1
.= Partial_Sums(s1).n + s1.(n+1) + Partial_Sums(s2).(n+1) by Def1
.= Partial_Sums(s1).n+s1.(n+1)+(s2.(n+1)+Partial_Sums(s2).n) by Def1
.= Partial_Sums(s1).n+(s1.(n+1)+s2.(n+1))+Partial_Sums(s2).n
.= Partial_Sums(s1).n+(s1+s2).(n+1)+Partial_Sums(s2).n by Lm1
.= Partial_Sums(s1).n+Partial_Sums(s2).n+(s1+s2).(n+1)
.= (Partial_Sums(s1)+Partial_Sums(s2)).n+(s1+s2).(n+1) by Lm1;
end;
(Partial_Sums(s1) + Partial_Sums(s2)).0 = Partial_Sums(s1).0 +
Partial_Sums(s2).0 by Lm1
.= s1.0 + Partial_Sums(s2).0 by Def1
.= s1.0 + s2.0 by Def1
.= (s1+s2).0 by Lm1;
hence thesis by A1,Def1;
end;
theorem Th6:
Partial_Sums(s1) - Partial_Sums(s2) = Partial_Sums(s1-s2)
proof
A1: now
let n;
thus (Partial_Sums(s1) - Partial_Sums(s2)).(n+1) = Partial_Sums(s1).(n+1)
- Partial_Sums(s2).(n+1) by RFUNCT_2:1
.= (Partial_Sums(s1).n + s1.(n+1)) - Partial_Sums(s2).(n+1) by Def1
.= (Partial_Sums(s1).n+s1.(n+1))-(s2.(n+1)+Partial_Sums(s2).n) by Def1
.= Partial_Sums(s1).n+(s1.(n+1)-s2.(n+1))-Partial_Sums(s2).n
.= (s1-s2).(n+1)+Partial_Sums(s1).n-Partial_Sums(s2).n by RFUNCT_2:1
.= (s1-s2).(n+1)+(Partial_Sums(s1).n-Partial_Sums(s2).n)
.= (Partial_Sums(s1)-Partial_Sums(s2)).n+(s1-s2).(n+1) by RFUNCT_2:1;
end;
(Partial_Sums(s1) - Partial_Sums(s2)).0 = Partial_Sums(s1).0 -
Partial_Sums(s2).0 by RFUNCT_2:1
.= s1.0 - Partial_Sums(s2).0 by Def1
.= s1.0 - s2.0 by Def1
.= (s1-s2).0 by RFUNCT_2:1;
hence thesis by A1,Def1;
end;
theorem
s1 is summable & s2 is summable implies s1+s2 is summable &
Sum(s1+s2) = Sum(s1) + Sum(s2)
proof
assume s1 is summable & s2 is summable;
then
A1: Partial_Sums(s1) is convergent & Partial_Sums(s2) is convergent;
then Partial_Sums(s1) + Partial_Sums(s2) is convergent;
then Partial_Sums(s1+s2) is convergent by Th5;
hence s1+s2 is summable;
thus Sum(s1+s2) =lim (Partial_Sums(s1) + Partial_Sums(s2)) by Th5
.=Sum(s1) + Sum(s2) by A1,SEQ_2:6;
end;
theorem
s1 is summable & s2 is summable implies s1-s2 is summable & Sum(s1-s2)
= Sum(s1) - Sum(s2)
proof
assume s1 is summable & s2 is summable;
then
A1: Partial_Sums(s1) is convergent & Partial_Sums(s2) is convergent;
then Partial_Sums(s1) - Partial_Sums(s2) is convergent;
then Partial_Sums(s1-s2) is convergent by Th6;
hence s1-s2 is summable;
thus Sum(s1-s2) =lim (Partial_Sums(s1) - Partial_Sums(s2)) by Th6
.=Sum(s1) - Sum(s2) by A1,SEQ_2:12;
end;
theorem Th9:
Partial_Sums(r(#)s) = r(#)Partial_Sums(s)
proof
A1: now
let n;
thus (r(#)Partial_Sums(s)).(n+1) = r*Partial_Sums(s).(n+1) by SEQ_1:9
.= r*(Partial_Sums(s).n + s.(n+1)) by Def1
.= r*Partial_Sums(s).n + r*s.(n+1)
.= (r(#)Partial_Sums(s)).n + r*s.(n+1) by SEQ_1:9
.= (r(#)Partial_Sums(s)).n + (r(#)s).(n+1) by SEQ_1:9;
end;
(r(#)Partial_Sums(s)).0 = r*Partial_Sums(s).0 by SEQ_1:9
.= r*s.0 by Def1
.= (r(#)s).0 by SEQ_1:9;
hence thesis by A1,Def1;
end;
theorem Th10:
s is summable implies r(#)s is summable & Sum(r(#)s) =r*Sum(s)
proof
assume s is summable;
then
A1: Partial_Sums(s) is convergent;
then r(#)Partial_Sums(s) is convergent;
then Partial_Sums(r(#)s) is convergent by Th9;
hence r(#)s is summable;
thus Sum(r(#)s) =lim (r(#)Partial_Sums(s)) by Th9
.=r*Sum(s) by A1,SEQ_2:8;
end;
theorem Th11:
for s,s1 st for n holds s1.n=s.0 holds Partial_Sums(s^\1) = (
Partial_Sums(s)^\1) - s1
proof
let s,s1;
assume
A1: for n holds s1.n=s.0;
A2: now
let k;
thus ((Partial_Sums(s)^\1) - s1).(k+1) = (Partial_Sums(s)^\1).(k+1) - s1.(
k+1) by RFUNCT_2:1
.= (Partial_Sums(s)^\1).(k+1) - s.0 by A1
.= Partial_Sums(s).(k+1+1) - s.0 by NAT_1:def 3
.= s.(k+1+1) + Partial_Sums(s).(k+1) - s.0 by Def1
.= s.(k+1+1) + Partial_Sums(s).(k+1) - s1.k by A1
.= s.(k+1+1) + (Partial_Sums(s).(k+1) - s1.k)
.= s.(k+1+1) + ((Partial_Sums(s)^\1).k - s1.k) by NAT_1:def 3
.= s.(k+1+1) + ((Partial_Sums(s)^\1) - s1).k by RFUNCT_2:1
.= ((Partial_Sums(s)^\1) - s1).k + (s^\1).(k+1) by NAT_1:def 3;
end;
((Partial_Sums(s)^\1) - s1).0 = (Partial_Sums(s)^\1).0 - s1.0 by RFUNCT_2:1
.= (Partial_Sums(s)^\1).0 - s.0 by A1
.= Partial_Sums(s).(0+1) - s.0 by NAT_1:def 3
.= Partial_Sums(s).0 + s.(0+1) - s.0 by Def1
.= s.(0+1) + s.0 - s.0 by Def1
.= (s^\1).0 by NAT_1:def 3;
hence thesis by A2,Def1;
end;
theorem Th12:
s is summable implies for n holds s^\n is summable
proof
defpred X[Nat] means s^\$1 is summable;
A1: for n st X[n] holds X[n+1]
proof
let n;
set s1 = seq_const((s^\n).0);
for k holds s1.k = (s^\n).0 by SEQ_1:57;
then
A2: Partial_Sums(s^\n^\1) = (Partial_Sums(s^\n)^\1) - s1 by Th11;
assume s^\n is summable;
then Partial_Sums(s^\n) is convergent;
then s^\(n+1)=(s^\n)^\1 & Partial_Sums(s^\n^\1) is convergent by A2,
NAT_1:48;
hence thesis by Def2;
end;
assume s is summable;
then
A3: X[0] by NAT_1:47;
thus for n holds X[n] from NAT_1:sch 2(A3,A1);
end;
theorem Th13:
(ex n st s^\n is summable) implies s is summable
proof
given n such that
A1: s^\n is summable;
reconsider PS = Partial_Sums(s).n as Element of REAL;
set s1 = seq_const Partial_Sums(s).n;
for k holds (Partial_Sums(s)^\(n+1)).k = Partial_Sums(s^\(n+1)).k + s1.k
proof
defpred X[Nat] means
(Partial_Sums(s)^\(n+1)).$1 = Partial_Sums
(s^\(n+1)).$1 + s1.$1;
A2: Partial_Sums(s^\(n+1)).0 = (s^\(n+1)).0 by Def1
.= s.(0+(n+1)) by NAT_1:def 3
.= s.(n+1);
A3: for k st X[k] holds X[k+1]
proof
let k;
assume
A4: (Partial_Sums(s)^\(n+1)).k = Partial_Sums(s^\(n+1)).k + s1.k;
Partial_Sums(s^\(n+1)).(k+1) + s1.(k+1) = s1.(k+1) + (Partial_Sums(
s^\(n+1)).k + (s^\(n+1)).(k+1)) by Def1
.= s1.(k+1) + Partial_Sums(s^\(n+1)).k + (s^\(n+1)).(k+1)
.= Partial_Sums(s).n + Partial_Sums(s^\(n+1)).k + (s^\(n+1)).(k+1)
by SEQ_1:57
.= (Partial_Sums(s)^\(n+1)).k + (s^\(n+1)).(k+1) by A4,SEQ_1:57
.= Partial_Sums(s).(k+(n+1)) + (s^\(n+1)).(k+1) by NAT_1:def 3
.= Partial_Sums(s).(k+(n+1)) + s.(k+1+(n+1)) by NAT_1:def 3
.= Partial_Sums(s).(k+(n+1)+1) by Def1
.= Partial_Sums(s).(k+1+(n+1))
.= (Partial_Sums(s)^\(n+1)).(k+1) by NAT_1:def 3;
hence thesis;
end;
(Partial_Sums(s)^\(n+1)).0 = Partial_Sums(s).(0+(n+1)) by NAT_1:def 3
.= s.(n+1) + Partial_Sums(s).n by Def1
.= Partial_Sums(s^\(n+1)).0 + s1.0 by A2,SEQ_1:57;
then
A5: X[0];
thus for k holds X[k] from NAT_1:sch 2(A5,A3);
end;
then
A6: Partial_Sums(s)^\(n+1) = Partial_Sums(s^\(n+1)) + s1 by SEQ_1:7
.= Partial_Sums((s^\n)^\1) + s1 by NAT_1:48;
s^\n^\1 is summable by A1,Th12;
then Partial_Sums(s^\n^\1) is convergent;
then Partial_Sums(s)^\(n+1) is convergent by A6;
then Partial_Sums(s) is convergent by SEQ_4:21;
hence thesis;
end;
theorem Th14:
(for n holds s1.n<=s2.n) implies for n holds Partial_Sums(s1).n
<=Partial_Sums(s2).n
proof
defpred X[Nat] means
Partial_Sums(s1).$1 <= Partial_Sums(s2).$1;
assume
A1: for n holds s1.n<=s2.n;
A2: for n st X[n] holds X[n+1]
proof
let n such that
A3: Partial_Sums(s1).n <= Partial_Sums(s2).n;
A4: s1.(n+1)<=s2.(n+1) by A1;
Partial_Sums(s1).(n+1) = Partial_Sums(s1).n + s1.(n+1) & Partial_Sums(
s2).(n +1) = Partial_Sums(s2).n + s2.(n+1) by Def1;
hence thesis by A3,A4,XREAL_1:7;
end;
Partial_Sums(s2).0 = s2.0 & Partial_Sums(s1).0 = s1.0 by Def1;
then
A5: X[0] by A1;
thus for n holds X[n] from NAT_1:sch 2(A5,A2);
end;
theorem
s is summable implies
for n holds Sum(s) = Partial_Sums(s).n + Sum(s^\(n+1))
proof
defpred X[Nat] means
Sum(s) = Partial_Sums(s).$1 + Sum(s^\($1+1));
assume
A1: s is summable;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume
A3: Sum(s) = Partial_Sums(s).n + Sum(s^\(n+1));
set s1 = seq_const (s^\(n+1)).0;
for k holds s1.k= (s^\(n+1)).0 by SEQ_1:57;
then
A4: Partial_Sums(s^\(n+1)^\1) = (Partial_Sums(s^\(n+1))^\1) - s1 by Th11;
s^\(n+1) is summable by A1,Th12;
then
A5: Partial_Sums(s^\(n+1)) is convergent;
lim Partial_Sums(s^\(n+1+1)) = lim Partial_Sums(s^\(n+1)^\1) by NAT_1:48
.= lim (Partial_Sums(s^\(n+1))^\1) - lim s1 by A5,A4,SEQ_2:12
.= lim Partial_Sums(s^\(n+1)) - lim s1 by A5,SEQ_4:20
.= Sum(s^\(n+1)) - s1.0 by SEQ_4:26
.= Sum(s^\(n+1)) - (s^\(n+1)).0 by SEQ_1:57;
then Sum(s^\(n+1+1)) = Sum(s) - (Partial_Sums(s).n + (s^\(n+1)).0) by A3
.= Sum(s) - (Partial_Sums(s).n + s.(0+(n+1))) by NAT_1:def 3
.= Sum(s) - Partial_Sums(s).(n+1) by Def1;
hence thesis;
end;
A6: X[0]
proof
set s1 = seq_const s.0;
A7: Partial_Sums(s) is convergent by A1;
for k holds s1.k= s.0 by SEQ_1:57;
then Partial_Sums(s^\1) = (Partial_Sums(s)^\1) - s1 by Th11;
then lim Partial_Sums(s^\1) = lim (Partial_Sums(s)^\1) - lim s1 by A7,
SEQ_2:12
.= lim Partial_Sums(s) - lim s1 by A7,SEQ_4:20
.= Sum(s) - s1.0 by SEQ_4:26
.= Sum(s) - s.0 by SEQ_1:57;
then Sum(s) = Sum(s^\1) +(-(-s.0));
hence thesis by Def1;
end;
thus for n holds X[n] from NAT_1:sch 2(A6,A2);
end;
theorem Th16:
(for n holds 0<=s.n) implies Partial_Sums(s) is non-decreasing
proof
assume
A1: for n holds 0<=s.n;
now
let n;
0<=s.(n+1) by A1;
then 0 + Partial_Sums(s).n <= s.(n+1) + Partial_Sums(s).n by XREAL_1:6;
hence Partial_Sums(s).n <= Partial_Sums(s).(n+1) by Def1;
end;
hence thesis;
end;
theorem Th17:
(for n holds 0<=s.n) implies (Partial_Sums(s) is bounded_above
iff s is summable)
proof
assume for n holds 0<=s.n;
then Partial_Sums(s) is non-decreasing by Th16;
hence Partial_Sums(s) is bounded_above implies s is summable;
assume s is summable;
then Partial_Sums(s) is convergent;
then Partial_Sums(s) is bounded;
hence thesis;
end;
theorem
s is summable & (for n holds 0<=s.n) implies 0<=Sum(s)
proof
assume that
A1: s is summable and
A2: for n holds 0<=s.n;
A3: now
let n;
A4: Partial_Sums(s).0 = s.0 by Def1;
Partial_Sums(s).0<=Partial_Sums(s).n & 0<=s.0 by A2,Th16,SEQM_3:11;
hence 0<=Partial_Sums(s).n by A4;
end;
Partial_Sums(s) is convergent by A1;
hence thesis by A3,SEQ_2:17;
end;
theorem Th19:
(for n holds 0<=s2.n) & s1 is summable & (ex m st for n st m<=n
holds s2.n<=s1.n) implies s2 is summable
proof
assume that
A1: for n holds 0<=s2.n and
A2: s1 is summable;
given m such that
A3: for n st m<=n holds s2.n<=s1.n;
s1^\m is summable by A2,Th12;
then Partial_Sums(s1^\m) is bounded_above;
then consider r being Real such that
A4: for n holds Partial_Sums(s1^\m).n<r by SEQ_2:def 3;
A5: now
let n;
s2.(n+m)<=s1.(n+m) by A3,NAT_1:12;
then (s2^\m).n<=s1.(n+m) by NAT_1:def 3;
hence (s2^\m).n<=(s1^\m).n by NAT_1:def 3;
end;
now
let n;
Partial_Sums(s2^\m).n <= Partial_Sums(s1^\m).n by A5,Th14;
hence Partial_Sums(s2^\m).n<r by A4,XXREAL_0:2;
end;
then
A6: Partial_Sums(s2^\m) is bounded_above by SEQ_2:def 3;
now
let n;
(s2^\m).n = s2.(n+m) by NAT_1:def 3;
hence 0<=(s2^\m).n by A1;
end;
then s2^\m is summable by A6,Th17;
hence thesis by Th13;
end;
theorem
(for n holds 0<=s1.n & s1.n<=s2.n) & s2 is summable implies s1 is
summable & Sum(s1)<=Sum(s2)
proof
assume that
A1: for n holds 0<=s1.n & s1.n<=s2.n and
A2: s2 is summable;
for n holds 0<=n implies s1.n<=s2.n by A1;
hence s1 is summable by A1,A2,Th19;
then
A3: Partial_Sums(s1) is convergent;
Partial_Sums(s2) is convergent & for n holds Partial_Sums(s1).n<=
Partial_Sums(s2).n by A1,A2,Th14;
hence thesis by A3,SEQ_2:18;
end;
theorem Th21:
s is summable iff for r st 0<r ex n st for m st n<=m holds |.
Partial_Sums(s).m - Partial_Sums(s).n.|<r
by SEQ_4:41;
::$N Sum of a Geometric Series
::$L https://en.wikipedia.org/wiki/Geometric_series Sum of a Geometric Series
theorem Th22:
a <> 1 implies Partial_Sums(a GeoSeq).n = (1 - a to_power (n+1)) /(1-a)
proof
defpred X[Nat] means
Partial_Sums(a GeoSeq).$1 = (1-a to_power ($1+1))/(1-a);
assume a<>1;
then
A1: 1-a <> 0;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(a GeoSeq).n = (1 - a to_power (n+1))/(1-a);
hence Partial_Sums(a GeoSeq).(n+1) = (1 - a to_power (n+1))/(1-a) + a
GeoSeq.(n+1) by Def1
.= (1 - a to_power (n+1))/(1-a) + a to_power (n+1) * 1 by PREPOWER:def 1
.= (1-a to_power (n+1))/(1-a)+a to_power (n+1)*((1-a)/(1-a)) by A1,
XCMPLX_1:60
.= (1-a to_power (n+1))/(1-a)+(a to_power (n+1)*(1-a))/(1-a)
.= (1-a to_power (n+1) + (a to_power (n+1)-a |^ (n+1)*a))/(1-a)
.= (1-a to_power (n+1) + (a to_power (n+1)-a |^ (n+1+1)))/(1-a) by
NEWTON:6
.= (1 - a to_power (n+1+1))/(1-a);
end;
Partial_Sums(a GeoSeq).0 = a GeoSeq.0 by Def1
.= 1 by PREPOWER:3
.= (1-a)/(1-a) by A1,XCMPLX_1:60
.= (1-a to_power (0+1))/(1-a);
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
a <> 1 & (for n holds s.(n+1) = a * s.n) implies for n holds
Partial_Sums(s).n = s.0 * (1 - a to_power (n+1))/(1-a)
proof
assume that
A1: a <> 1 and
A2: for n holds s.(n+1) = a * s.n;
defpred X[Nat] means s.$1 = s.0 * a GeoSeq.$1;
A3: for n st X[n] holds X[n+1]
proof
let n;
assume s.n = s.0 * a GeoSeq.n;
then s.(n+1) = a * (s.0 * a GeoSeq.n) by A2
.= s.0 * (a GeoSeq.n * a)
.= s.0 * a GeoSeq.(n+1) by PREPOWER:3;
hence thesis;
end;
a GeoSeq.0 = 1 by PREPOWER:3;
then
A4: X[0];
for n holds X[n] from NAT_1:sch 2(A4,A3);
then s = s.0 (#) a GeoSeq by SEQ_1:9;
then
A5: Partial_Sums(s) = s.0 (#) Partial_Sums(a GeoSeq) by Th9;
now
let n;
thus Partial_Sums(s).n = s.0 * Partial_Sums(a GeoSeq).n by A5,SEQ_1:9
.= s.0 * ((1 - a to_power (n+1))/(1-a)) by A1,Th22
.= s.0 * (1 - a to_power (n+1))/(1-a);
end;
hence thesis;
end;
theorem Th24:
|.a.|<1 implies a GeoSeq is summable & Sum(a GeoSeq) = 1/(1-a)
proof
deffunc U(Nat) = a to_power ($1+1);
consider s such that
A1: for n holds s.n = U(n) from SEQ_1:sch 1;
assume
A2: |.a.|<1;
then
A3: s is convergent & lim s = 0 by A1,Th3;
A4: now
a<1 by A2,SEQ_2:1;
then
A5: 1-a>0 by XREAL_1:50;
let r be Real;
assume r>0;
then r*(1-a)>0*r by A5;
then consider m such that
A6: for n st n>=m holds |.s.n - 0.|<r*(1-a) by A3,SEQ_2:def 7;
take m;
let n;
assume n>=m;
then |.s.n - 0.|<r*(1-a) by A6;
then |.a to_power (n+1) - 0.|<r*(1-a) by A1;
then
A7: |.a to_power (n+1).|/(1-a)<r*(1-a)/(1-a) by A5,XREAL_1:74;
a<>1 by A2,SEQ_2:1;
then
A8: |.Partial_Sums(a GeoSeq).n - 1/(1-a).| = |.(1 - a to_power (n+1))/
(1-a) - 1/(1-a).| by Th22
.= |.(1 +- a to_power (n+1) - 1)/(1-a).|
.= |.- a to_power (n+1)/(1-a).|
.= |.a to_power (n+1)/(1-a).| by COMPLEX1:52
.= |.a to_power (n+1).|/|.(1-a).| by COMPLEX1:67
.= |.a to_power (n+1).|/(1-a) by A5,ABSVALUE:def 1;
1-a<>0 by A2,SEQ_2:1;
hence |.Partial_Sums(a GeoSeq).n - 1/(1-a).| < r by A8,A7,XCMPLX_1:89;
end;
then
A9: Partial_Sums(a GeoSeq) is convergent by SEQ_2:def 6;
hence a GeoSeq is summable;
thus thesis by A4,A9,SEQ_2:def 7;
end;
theorem
|.a.| < 1 & (for n holds s.(n+1) = a * s.n) implies s is summable &
Sum(s) = s.0/(1-a)
proof
assume that
A1: |.a.| < 1 and
A2: for n holds s.(n+1) = a * s.n;
defpred X[Nat] means s.$1 = s.0 * a GeoSeq.$1;
A3: for n st X[n] holds X[n+1]
proof
let n;
assume s.n = s.0 * a GeoSeq.n;
then s.(n+1) = a * (s.0 * a GeoSeq.n) by A2
.= s.0 * (a GeoSeq.n * a)
.= s.0 * a GeoSeq.(n+1) by PREPOWER:3;
hence thesis;
end;
a GeoSeq.0 = 1 by PREPOWER:3;
then
A4: X[0];
for n holds X[n] from NAT_1:sch 2(A4,A3);
then s = s.0 (#) a GeoSeq by SEQ_1:9;
then
A5: Partial_Sums(s) = s.0 (#) Partial_Sums(a GeoSeq) by Th9;
a GeoSeq is summable by A1,Th24;
then
A6: Partial_Sums(a GeoSeq) is convergent;
then Partial_Sums(s) is convergent by A5;
hence s is summable;
Sum(a GeoSeq) = 1/(1-a) by A1,Th24;
then lim Partial_Sums(s) = s.0 * (1/(1-a)) by A5,A6,SEQ_2:8
.= s.0*1/(1-a)
.= s.0/(1-a);
hence thesis;
end;
theorem Th26:
(for n holds s.n>0 & s1.n=s.(n+1)/s.n) & s1 is convergent & lim
s1 < 1 implies s is summable
proof
assume that
A1: for n holds s.n>0 & s1.n=s.(n+1)/s.n and
A2: s1 is convergent and
A3: lim s1 < 1;
set r = (1 - lim s1)/2;
0 + lim s1 < 1 by A3;
then 0 < 1 - lim s1 by XREAL_1:20;
then r > 0;
then consider m such that
A4: for n st m <= n holds |.s1.n - lim s1.| < r by A2,SEQ_2:def 7;
set s2 = (s.m * (1-r) to_power (-m)) (#) (1-r) GeoSeq;
defpred X[Nat] means s.(m+$1) <= s2.(m+$1);
A5: now
let n;
s.n > 0 & s.(n+1) > 0 by A1;
then s.(n+1)/s.n > 0;
hence s1.n >= 0 by A1;
end;
then
A6: lim s1 >= 0 by A2,PREPOWER:1;
then 1 + -lim s1 < 1 + 1 by XREAL_1:6;
then
A7: (1 - lim s1)/2 < 2/2 by XREAL_1:74;
A8: r + lim s1 = 1 - r;
A9: for k holds X[k] implies X[k+1]
proof
set X = (s.m * (1-r) to_power (-m));
let k such that
A10: s.(m+k) <= s2.(m+k);
|.s1.(m+k) - lim s1.| < r by A4,NAT_1:11;
then s1.(m+k) - lim s1 < r by SEQ_2:1;
then
A11: s1.(m+k) <= 1 - r by A8,XREAL_1:19;
s2.(m+k) >= 0 by A1,A10;
then
A12: s1.(m+k) * s2.(m+k) <= (1-r) * s2.(m+k) by A11,XREAL_1:64;
s.(m+k) <> 0 by A1;
then
A13: s.(m+(k+1)) = s.(m+k+1) / s.(m+k) * s.(m+k) by XCMPLX_1:87
.= s1.(m+k) * s.(m+k) by A1;
s1.(m+k) >= 0 by A5;
then
A14: s.(m+(k+1)) <= s1.(m+k) * s2.(m+k) by A10,A13,XREAL_1:64;
(1-r) * s2.(m+k) = (1-r) * (X * (1-r) GeoSeq.(m+k)) by SEQ_1:9
.= X * ((1-r) GeoSeq.(m+k) * (1-r))
.= X * (1-r) GeoSeq.(m+k+1) by PREPOWER:3
.= s2.(m+(k+1)) by SEQ_1:9;
hence thesis by A14,A12,XXREAL_0:2;
end;
s2.(m+0) = (s.m * (1-r) to_power (-m)) * (1-r) GeoSeq.m by SEQ_1:9
.= (s.m * (1-r) to_power (-m)) * (1-r) |^ m by PREPOWER:def 1
.= s.m * ((1-r) to_power (-m) * (1-r) to_power m)
.= s.m * (1-r) to_power (-m + m) by A7,POWER:27,XREAL_1:50
.= s.m * 1 by POWER:24
.= s.(m+0);
then
A15: X[0];
A16: for k holds X[k] from NAT_1:sch 2(A15,A9);
A17: now
let n;
assume m <= n;
then consider k be Nat such that
A18: n = m + k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
n = m+k by A18;
hence s.n <= s2.n by A16;
end;
1 - lim s1 <= 1 - 0 by A6,XREAL_1:6;
then 1 - lim s1 < 2 * 2 by XXREAL_0:2;
then r < 2 * 2 / 2 by XREAL_1:74;
then r < 1 + 1;
then r - 1 < 1 by XREAL_1:19;
then
A19: - (r - 1) > - 1 by XREAL_1:24;
1 - lim s1 > 0 by A3,XREAL_1:50;
then r > 0;
then 1 - r < 1 - 0 by XREAL_1:10;
then |.1-r.| < 1 by A19,SEQ_2:1;
then (1-r) GeoSeq is summable by Th24;
then
A20: s2 is summable by Th10;
for n holds 0 <= s.n by A1;
hence thesis by A20,A17,Th19;
end;
theorem
(for n holds s.n>0) & (ex m st for n st n>=m holds s.(n+1)/s.n >= 1)
implies s is not summable
proof
assume that
A1: for n holds s.n>0 and
A2: ex m st for n st n>=m holds s.(n+1)/s.n >= 1;
consider m such that
A3: for n st n>=m holds s.(n+1)/s.n>=1 by A2;
defpred X[Nat] means s.(m+$1)>=s.m;
A4: for k st X[k] holds X[k+1]
proof
let k such that
A5: s.(m+k)>=s.m;
s.(m+k)>0 & s.(m+k+1)/s.(m+k)>=1 by A1,A3,NAT_1:11;
then s.(m+k+1)>=s.(m+k) by XREAL_1:191;
hence thesis by A5,XXREAL_0:2;
end;
A6: X[0];
A7: for k holds X[k] from NAT_1:sch 2(A6,A4);
A8: for k ex n st n>=k & not |.s.n - 0.|<s.m
proof
let k;
take n = m + k;
s.n>=s.m by A7;
hence thesis by NAT_1:11,SEQ_2:1;
end;
s.m>0 by A1;
then not lim s = 0 or s is not convergent by A8,SEQ_2:def 7;
hence thesis by Th4;
end;
theorem Th28:
(for n holds s.n>=0 & s1.n = n-root (s.n)) & s1 is convergent &
lim s1 < 1 implies s is summable
proof
assume that
A1: for n holds s.n>=0 & s1.n = n-root (s.n) and
A2: s1 is convergent and
A3: lim s1 < 1;
A4: now
let n;
A5: (s1^\1).n = s1.(n+1) by NAT_1:def 3
.= (n+1)-root (s.(n+1)) by A1;
s.(n+1) >= 0 by A1;
hence (s1^\1).n >= 0 by A5,NAT_1:11,POWER:7;
end;
set r = (1 - lim s1)/2;
0 + lim s1 < 1 by A3;
then 0 < 1 - lim s1 by XREAL_1:20;
then r > 0;
then consider m such that
A6: for n st m <= n holds |.s1.n - lim s1.| < r by A2,SEQ_2:def 7;
lim (s1^\1) = lim s1 by A2,SEQ_4:20;
then
A7: lim s1 >= 0 by A2,A4,PREPOWER:1;
then 1 + -lim s1 < 1 + 1 by XREAL_1:6;
then (1 - lim s1)/2 < 2/2 by XREAL_1:74;
then
A8: 1 - r > 0 by XREAL_1:50;
set s2 = (1-r) GeoSeq;
A9: r + lim s1 = 1 - r;
A10: for n st m+1<=n holds s.n <= (1-r) to_power n
proof
let n;
assume
A11: m+1<=n;
1<=m+1 by NAT_1:11;
then
A12: 1 <= n by A11,XXREAL_0:2;
A13: s.n >= 0 by A1;
m<=n by A11,NAT_1:13;
then |.s1.n - lim s1.| < r by A6;
then s1.n - lim s1 < r by SEQ_2:1;
then s1.n < 1 - r by A9,XREAL_1:19;
then
A14: n-root (s.n) < 1 - r by A1;
now
per cases;
suppose
s.n = 0;
hence s.n < (1 - r) to_power n by A8,POWER:34;
end;
suppose
s.n <> 0;
then n -Root (s.n) > 0 by A12,A13,PREPOWER:def 2;
then n-root (s.n) > 0 by A12,A13,POWER:def 1;
then (n-root (s.n)) to_power n < (1-r) to_power n by A11,A14,POWER:37;
hence s.n < (1-r) to_power n by A12,A13,POWER:4;
end;
end;
hence thesis;
end;
A15: for n st m+1 <= n holds s.n <= s2.n
proof
let n;
s2.n = (1-r) to_power n by PREPOWER:def 1;
hence thesis by A10;
end;
1 - lim s1 <= 1 - 0 by A7,XREAL_1:6;
then 1 - lim s1 < 2 * 2 by XXREAL_0:2;
then r < 2 * 2 / 2 by XREAL_1:74;
then r < 1 + 1;
then r - 1 < 1 by XREAL_1:19;
then
A16: - (r - 1) > - 1 by XREAL_1:24;
1 - lim s1 > 0 by A3,XREAL_1:50;
then r > 0;
then 1 - r < 1 - 0 by XREAL_1:10;
then |.1-r.| < 1 by A16,SEQ_2:1;
then s2 is summable by Th24;
hence thesis by A1,A15,Th19;
end;
theorem Th29:
(for n holds s.n>=0 & s1.n = n-root (s.n)) & (ex m st for n st m
<=n holds s1.n>=1) implies s is not summable
proof
assume that
A1: for n holds s.n>=0 & s1.n = n-root (s.n) and
A2: ex m st for n st m<=n holds s1.n>=1;
consider m such that
A3: for n st m<=n holds s1.n>=1 by A2;
A4: for n st m+1<=n holds s.n>=1
proof
let n such that
A5: m+1<=n;
1<=1+m by NAT_1:11;
then
A6: 1<=n by A5,XXREAL_0:2;
A7: s.n >= 0 by A1;
m<=m+1 by NAT_1:11;
then m<=n by A5,XXREAL_0:2;
then s1.n >= 1 by A3;
then
A8: n-root (s.n) >= 1 by A1;
now
per cases by A8,XXREAL_0:1;
suppose
n-root (s.n) = 1;
then s.n = 1 |^ n by A6,A7,POWER:4;
hence thesis;
end;
suppose
n-root (s.n) > 1;
then (n-root (s.n)) to_power n > 1 by A5,POWER:35;
hence thesis by A6,A7,POWER:4;
end;
end;
hence thesis;
end;
for k ex n st k<=n & not |.s.n - 0.| < 1
proof
let k;
take n = m + 1 + k;
not s.n < 1 by A4,NAT_1:11;
hence thesis by NAT_1:11,SEQ_2:1;
end;
then s is not convergent or not lim s = 0 by SEQ_2:def 7;
hence thesis by Th4;
end;
theorem
(for n holds s.n>=0 & s1.n = n-root (s.n)) & s1 is convergent & lim s1
> 1 implies s is not summable
proof
assume that
A1: for n holds s.n>=0 & s1.n = n-root (s.n) and
A2: s1 is convergent and
A3: lim s1 > 1;
set r = lim s1 - 1;
r > 0 by A3,XREAL_1:50;
then consider m such that
A4: for n st m<=n holds |.s1.n - lim s1.| < r by A2,SEQ_2:def 7;
for n st m<=n holds s1.n >= 1
proof
let n;
assume m<=n;
then |.s1.n - lim s1.| < r by A4;
then s1.n - lim s1 > - r by SEQ_2:1;
then s1.n - lim s1 + lim s1 > - r + lim s1 by XREAL_1:6;
hence thesis;
end;
hence thesis by A1,Th29;
end;
registration
let k, n be Nat;
cluster k to_power n -> natural;
coherence;
end;
definition
let k, n be Nat;
redefine func k to_power n -> Element of NAT; :: redefines to_power (POWER, definition)
coherence by ORDINAL1:def 12;
end;
theorem Th31:
s is non-increasing & (for n holds s.n>=0 & s1.n = 2 to_power n
* s.(2 to_power n)) implies (s is summable iff s1 is summable)
proof
assume that
A1: s is non-increasing and
A2: for n holds s.n>=0 & s1.n = 2 to_power n * s.(2 to_power n);
A3: Partial_Sums(s).(2 to_power (0+1)) = Partial_Sums(s).(1+1)
.= Partial_Sums(s).(0+1)+s.2 by Def1
.= Partial_Sums(s).0+s.1+s.2 by Def1
.= s.0+s.1+s.2 by Def1;
A4: now
let n;
s.(2 to_power n) >= 0 by A2;
then 2 to_power n * s.(2 to_power n) >= 0;
hence s1.n >= 0 by A2;
end;
thus s is summable implies s1 is summable
proof
defpred Y[Nat] means
Partial_Sums(s1).$1 <= 2 * Partial_Sums(s)
.(2 to_power $1);
A5: s.0>=0 by A2;
A6: for n st Y[n] holds Y[n+1]
proof
let n;
deffunc U(Nat) = Partial_Sums(s).(2 to_power n + $1) -
Partial_Sums(s).(2 to_power n);
consider a being Real_Sequence such that
A7: for m holds a.m = U(m) from SEQ_1:sch 1;
defpred X[Nat] means
$1 > 2 to_power n or $1 * s.(2 to_power
(n+1)) <= a.$1;
A8: for m st X[m] holds X[m+1]
proof
let m;
assume
A9: m > 2 to_power n or m * s.(2 to_power (n+1)) <= a.m;
now
per cases by A9;
suppose
m > 2 to_power n;
hence thesis by NAT_1:13;
end;
suppose
A10: m * s.(2 to_power (n+1)) <= a.m;
now
per cases;
suppose
m<2 to_power n;
then m+1<=2 to_power n by NAT_1:13;
then 2 to_power n + (m+1) <= 2 to_power n + 2 to_power n by
XREAL_1:7;
then 2 to_power n + m + 1 <= 2 * 2 to_power n;
then 2 to_power n + m + 1 <= 2 to_power 1 * 2 to_power n;
then 2 to_power n + m + 1 <= 2 to_power (n+1) by POWER:27;
then s.(2 to_power n + m + 1) >= s.(2 to_power (n+1)) by A1,
SEQM_3:8;
then
m * s.(2 to_power (n+1)) + 1 * s.(2 to_power (n+1)) <= a.
m + s.(2 to_power n + m + 1) by A10,XREAL_1:7;
then (m + 1) * s.(2 to_power (n+1)) <= Partial_Sums(s).(2
to_power n + m) - Partial_Sums(s).(2 to_power n) + s.(2 to_power n + m + 1) by
A7;
then (m + 1) * s.(2 to_power (n+1)) <= Partial_Sums(s).(2
to_power n + m) + s.(2 to_power n + m + 1) - Partial_Sums(s).(2 to_power n);
then (m + 1) * s.(2 to_power (n+1)) <= Partial_Sums(s).(2
to_power n + (m + 1)) - Partial_Sums(s).(2 to_power n) by Def1;
hence thesis by A7;
end;
suppose
m>=2 to_power n;
hence thesis by NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
a.0 = Partial_Sums(s).(2 to_power n + 0) - Partial_Sums(s).(2
to_power n) by A7
.= 0;
then
A11: X[0];
for m holds X[m] from NAT_1:sch 2(A11,A8);
then 2*(2 to_power n * s.(2 to_power (n+1))) <= 2*a.(2 to_power n) by
XREAL_1:64;
then 2*2 to_power n * s.(2 to_power (n+1)) <= 2*a.(2 to_power n);
then 2 to_power 1 * 2 to_power n * s.(2 to_power (n+1)) <= 2*a.(2
to_power n);
then 2 to_power (n+1) * s.(2 to_power (n+1)) <= 2*a.(2 to_power n) by
POWER:27;
then s1.(n+1) <= 2*a.(2 to_power n) by A2;
then s1.(n+1) <= 2*(Partial_Sums(s).(2 to_power n + 2 to_power n) -
Partial_Sums(s).(2 to_power n)) by A7;
then
A12: 2 * Partial_Sums(s).(2 to_power n) + s1.(n+1) <= 2 * Partial_Sums(s
).(2 to_power n) + (2*(Partial_Sums(s).(2 to_power n + 2 to_power n) -
Partial_Sums(s).(2 to_power n))) by XREAL_1:7;
assume Partial_Sums(s1).n <= 2 * Partial_Sums(s).(2 to_power n);
then
Partial_Sums(s1).n + s1.(n+1) <= 2 * Partial_Sums(s).(2 to_power n)
+ s1.(n+1) by XREAL_1:6;
then
A13: Partial_Sums(s1).(n+1) <= 2 * Partial_Sums(s).(2 to_power n) + s1.(
n+1) by Def1;
2 to_power n + 2 to_power n = 2 * 2 to_power n
.= 2 to_power 1 * 2 to_power n
.= 2 to_power (n+1) by POWER:27;
hence thesis by A13,A12,XXREAL_0:2;
end;
A14: 2 to_power 0 = 0+1 by POWER:24;
then
A15: 2 * Partial_Sums(s).(2 to_power 0) = 2 * (Partial_Sums(s).0 + s.1) by Def1
.= 2*(s.0 + s.1) by Def1
.= 2*s.0 + 2*s.1;
assume s is summable;
then Partial_Sums(s) is bounded_above;
then consider r be Real such that
A16: for n holds Partial_Sums(s).n<r by SEQ_2:def 3;
s.1>=0 by A2;
then
A17: s.1 + s.1 >= s.1 + 0 by XREAL_1:7;
Partial_Sums(s1).0 = s1.0 by Def1
.= 1 * s.1 by A2,A14
.= s.1;
then
A18: Y[0] by A15,A17,A5,XREAL_1:7;
A19: for n holds Y[n] from NAT_1:sch 2(A18,A6);
now
let n;
2 * Partial_Sums(s).(2 to_power n) < 2*r & Partial_Sums(s1).n <= 2
* Partial_Sums(s).(2 to_power n) by A19,A16,XREAL_1:68;
hence Partial_Sums(s1).n < 2*r by XXREAL_0:2;
end;
then Partial_Sums(s1) is bounded_above by SEQ_2:def 3;
hence thesis by A4,Th17;
end;
assume s1 is summable;
then Partial_Sums(s1) is bounded_above;
then consider r be Real such that
A20: for n holds Partial_Sums(s1).n<r by SEQ_2:def 3;
A21: 2 to_power 0 = 1 by POWER:24;
defpred Y[Nat] means
Partial_Sums(s).(2 to_power ($1+1)) <=
Partial_Sums(s1).$1 + s.0 + s.2;
A22: for n st Y[n] holds Y[n+1]
proof
let n;
defpred X[Nat] means
Partial_Sums(s).(2 to_power (n+1) + $1) -
Partial_Sums(s).(2 to_power (n+1)) <= $1 * s.(2 to_power (n+1));
A23: for m st X[m] holds X[m+1]
proof
let m;
2 to_power (n+1) + (m+1) >= 2 to_power (n+1) by NAT_1:11;
then
A24: s.(2 to_power (n+1) + (m+1)) <= s.(2 to_power (n+1)) by A1,SEQM_3:8;
assume Partial_Sums(s).(2 to_power (n+1) + m) - Partial_Sums(s).(2
to_power (n+1)) <= m * s.(2 to_power (n+1));
then Partial_Sums(s).(2 to_power (n+1) + m) - Partial_Sums(s).(2
to_power (n+1)) + s.(2 to_power (n+1) + m+1) <= m * s.(2 to_power (n+1)) + s.(2
to_power (n+1)) by A24,XREAL_1:7;
then
Partial_Sums(s).(2 to_power (n+1) + m) + s.(2 to_power (n+1) + m+1)
- Partial_Sums(s).(2 to_power (n+1)) <= m * s.(2 to_power (n+1)) + s.(2
to_power (n+1));
hence thesis by Def1;
end;
A25: X[0];
for m holds X[m] from NAT_1:sch 2(A25,A23);
then
Partial_Sums(s).(2 to_power (n+1) + 2 to_power (n+1)) - Partial_Sums(
s).(2 to_power (n+1))<= 2 to_power (n+1) * s.(2 to_power (n+1));
then
A26: Partial_Sums(s).(2 to_power (n+1) + 2 to_power (n+1)) - Partial_Sums(
s).(2 to_power (n+1)) <= s1.(n+1) by A2;
assume Partial_Sums(s).(2 to_power (n+1)) <= Partial_Sums(s1).n + s.0+s. 2;
then Partial_Sums(s).(2 to_power (n+1)) + s1.(n+1) <= s1.(n+1) + (
Partial_Sums(s1).n + s.0+s.2) by XREAL_1:7;
then
Partial_Sums(s).(2 to_power (n+1)) + s1.(n+1) <= Partial_Sums(s1).n +
s1.(n+1) + s.0+s.2;
then
A27: Partial_Sums(s).(2 to_power (n+1)) + s1.(n+1) <= Partial_Sums(s1).(n+
1) + s.0+s.2 by Def1;
2 to_power (n+1) + 2 to_power (n+1) = 2 * 2 to_power (n+1)
.= 2 to_power 1 * 2 to_power (n+1)
.= 2 to_power (n+1+1) by POWER:27;
then
Partial_Sums(s).(2 to_power (n+1+1)) - Partial_Sums(s).(2 to_power (n
+1)) + Partial_Sums(s).(2 to_power (n+1)) <= Partial_Sums(s).(2 to_power (n+1))
+ s1.(n+1) by A26,XREAL_1:7;
hence thesis by A27,XXREAL_0:2;
end;
Partial_Sums(s1).0 + s.0 + s.2 = s1.0 + s.0 + s.2 by Def1
.= 2 to_power 0 * s.(2 to_power 0) + s.0 + s.2 by A2
.= s.0 + s.1 + s.2 by A21;
then
A28: Y[0] by A3;
A29: for n holds Y[n] from NAT_1:sch 2(A28,A22);
A30: Partial_Sums(s) is non-decreasing by A2,Th16;
now
let n;
Partial_Sums(s1).n < r by A20;
then
A31: Partial_Sums(s1).n + (s.0 + s.2) < r + (s.0+s.2) by XREAL_1:6;
(1+1) to_power n >= 1 + n*1 & 1+n>=n by NAT_1:11,POWER:49;
then 2 to_power n >= n by XXREAL_0:2;
then 2 to_power n + 2 to_power n>= n+n by XREAL_1:7;
then 2 * 2 to_power n >= n+n;
then 2 to_power 1 * 2 to_power n >= n+n;
then
A32: 2 to_power (n+1) >= n+n by POWER:27;
n+n>=n by NAT_1:11;
then 2 to_power (n+1) >= n by A32,XXREAL_0:2;
then
A33: Partial_Sums(s).(2 to_power (n+1)) >= Partial_Sums(s).n by A30,SEQM_3:6;
Partial_Sums(s).(2 to_power (n+1)) <= Partial_Sums(s1).n+s.0+s.2 by A29;
then Partial_Sums(s).n <= Partial_Sums(s1).n+s.0+s.2 by A33,XXREAL_0:2;
hence Partial_Sums(s).n < r + (s.0+s.2) by A31,XXREAL_0:2;
end;
then Partial_Sums(s) is bounded_above by SEQ_2:def 3;
hence thesis by A2,Th17;
end;
Lm2: 1 in REAL by XREAL_0:def 1;
theorem
p>1 & (for n st n>=1 holds s.n = 1/n to_power p) implies s is summable
proof
assume that
A1: p>1 and
A2: for n st n>=1 holds s.n = 1/n to_power p;
defpred X[Nat,Real] means ($1=0 & $2=1) or ($1>=1 & $2=1/
$1 to_power p);
A3: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof
let n be Element of NAT;
A4: n <> 0 implies n >= 0+1 by NAT_1:13;
per cases;
suppose
A5: n = 0;
reconsider jj = 1 as Real;
take jj;
thus thesis by A5,Lm2;
end;
suppose
A6: n > 0;
reconsider n1 = 1/n to_power p as Element of REAL by XREAL_0:def 1;
take n1;
thus thesis by A6,A4;
end;
end;
consider s1 such that
A7: for n being Element of NAT holds X[n,s1.n] from FUNCT_2:sch 3(A3);
deffunc V(Nat) = 2 to_power $1 * s1.(2 to_power $1);
consider s2 such that
A8: for n holds s2.n = V(n) from SEQ_1:sch 1;
A9: s1.0 = 1 by A7;
now
let n;
now
per cases by NAT_1:6;
suppose
A10: n=0;
then (n+1) #R p >= 1 by A1,PREPOWER:85;
then
A11: (n+1) to_power p >= 1 by POWER:def 2;
s1.(n+1) = 1/(n+1) to_power p by A7;
hence s1.(n+1)<=s1.n by A9,A10,A11,XREAL_1:211;
end;
suppose
A12: ex m be Nat st n=m+1;
A13: n in NAT by ORDINAL1:def 12;
n to_power p > 0 by POWER:34,A12;
then 1/n to_power p > 0;
then
A14: s1.n>0 by A7,A13;
A15: n/(n+1)<=1 by NAT_1:11,XREAL_1:183;
A16: n/(n+1)>0 by A12;
s1.(n+1)/s1.n = (1/(n+1) to_power p)/s1.n by A7
.= (1/(n+1) to_power p)/(1/n to_power p) by A7,A12
.= (1/(n+1) to_power p) * n to_power p
.= n to_power p / (n+1) to_power p
.= (n/(n+1)) to_power p by A12,POWER:31
.= (n/(n+1)) #R p by A16,POWER:def 2;
then s1.(n+1)/s1.n <= (n/(n+1)) #R 0 by A1,A16,A15,PREPOWER:84;
then s1.(n+1)/s1.n <= 1 by A12,PREPOWER:71;
hence s1.(n+1)<=s1.n by A14,XREAL_1:187;
end;
end;
hence s1.(n+1)<=s1.n;
end;
then
A17: s1 is non-increasing;
A18: now
let n;
assume n>=0;
A19: n+1>=0+1 by XREAL_1:6;
(s^\1).n = s.(n+1) by NAT_1:def 3
.= 1/(n+1) to_power p by A2,A19
.= s1.(n+1) by A7
.= (s1^\1).n by NAT_1:def 3;
hence (s1^\1).n>=(s^\1).n;
end;
deffunc U(Nat) = $1-root (s2.$1);
consider s3 such that
A20: for n holds s3.n = U(n) from SEQ_1:sch 1;
A21: now
let n;
A22: 2 to_power n > 0 by POWER:34;
thus
A23: s2.n = 2 to_power n * s1.(2 to_power n) by A8
.= 2 to_power n * (1/(2 to_power n) to_power p) by A7,A22
.= 2 to_power n * (1/2 to_power (n*p)) by POWER:33
.= 2 to_power n * 2 to_power (-n*p) by POWER:28
.= 2 to_power (n+-n*p) by POWER:27
.= 2 to_power ((1-p)*n);
hence s2.n>=0 by POWER:34;
s2.n = 2 to_power (1-p) to_power n by A23,POWER:33;
hence s3.n = n-root (2 to_power (1-p) to_power n) by A20;
end;
A0: 2 to_power (1-p) is set by TARSKI:1;
A24: now
let n be Nat;
A25: n+1>=0+1 & 2 to_power (1-p) >= 0 by POWER:34,XREAL_1:6;
thus (s3^\1).n = s3.(n+1) by NAT_1:def 3
.= (n+1)-root (2 to_power (1-p) to_power (n+1)) by A21
.= 2 to_power (1-p) by A25,POWER:4;
end;
then
A26: s3^\1 is constant by A0;
then lim (s3^\1) = (s3^\1).0 by SEQ_4:26
.= 2 to_power (1-p) by A24;
then
A27: lim s3 = 2 to_power (1-p) by A26,SEQ_4:22;
A28: now
let n;
now
per cases by NAT_1:6;
suppose
n=0;
hence s1.n >= 0 by A7;
end;
suppose
A29: ex m be Nat st n=m+1;
A30: n in NAT by ORDINAL1:def 12;
n to_power p > 0 by POWER:34,A29;
then 1/n to_power p >= 0;
hence s1.n>=0 by A7,A30;
end;
end;
hence s1.n>=0 & s2.n = 2 to_power n * s1.(2 to_power n) by A8;
end;
A31: now
let n;
A32: n+1>=0+1 by XREAL_1:6;
A33: s1.(n+1)>=0 by A28;
(s^\1).n = s.(n+1) by NAT_1:def 3
.= 1/(n+1) to_power p by A2,A32
.= s1.(n+1) by A7
.= (s1^\1).n by NAT_1:def 3;
hence (s^\1).n>=0 by A33,NAT_1:def 3;
end;
A34: s3 is convergent by A26,SEQ_4:21;
1-p<0 by A1,XREAL_1:49;
then lim s3 < 1 by A27,POWER:36;
then s2 is summable by A20,A21,A34,Th28;
then s1 is summable by A17,A28,Th31;
then s1^\1 is summable by Th12;
then s^\1 is summable by A31,A18,Th19;
hence thesis by Th13;
end;
::$N Divergence of the Harmonic Series
::$L https://en.wikipedia.org/wiki/Harmonic_series_(mathematics) Divergence of the Harmonic Series
theorem
p <= 1 & (for n st n>=1 holds s.n=1/n to_power p) implies s is not summable
proof
assume that
A1: p<=1 and
A2: for n st n>=1 holds s.n = 1/n to_power p;
per cases;
suppose
A3: p<0;
now
assume s is convergent & lim s=0;
then consider m such that
A4: for n st n>= m holds |.s.n-0.|<1 by SEQ_2:def 7;
consider k such that
A5: k>m by SEQ_4:3;
now
let n such that
A6: n>=k;
A7: n>0 by A5,A6;
then
A8: n>=0+1 by NAT_1:13;
n>=m by A5,A6,XXREAL_0:2;
then |.s.n-0.|<1 by A4;
then |.1/n to_power p.|<1 by A2,A8;
then |.n to_power (-p).|<1 by A7,POWER:28;
then
A9: n to_power (-p)<1 by ABSVALUE:def 1;
n #R (-p) >= 1 by A3,A8,PREPOWER:85;
hence contradiction by A7,A9,POWER:def 2;
end;
hence contradiction;
end;
hence thesis by Th4;
end;
suppose
A10: p>=0;
defpred X[Element of NAT,Real] means ($1=0 & $2=1) or ($1>=1 & $2
=1/$1 to_power p);
A11: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n be Element of NAT;
A12: n <> 0 implies n >= 0+1 by NAT_1:13;
per cases;
suppose
A13: n = 0;
reconsider jj = 1 as Real;
take jj;
thus thesis by A13,Lm2;
end;
suppose
A14: n > 0;
reconsider n1 = 1/n to_power p as Element of REAL by XREAL_0:def 1;
take n1;
thus thesis by A14,A12;
end;
end;
consider s1 such that
A15: for n being Element of NAT holds X[n,s1.n] from FUNCT_2:sch 3(A11);
A16: s1.0 = 1 by A15;
now
let n;
now
per cases by NAT_1:6;
suppose
A17: n=0;
then (n+1) #R p >= 1 by A10,PREPOWER:85;
then
A18: (n+1) to_power p >= 1 by POWER:def 2;
s1.(n+1) = 1/(n+1) to_power p by A15;
hence s1.(n+1)<=s1.n by A16,A17,A18,XREAL_1:211;
end;
suppose
A19: ex m be Nat st n=m+1;
A20: n in NAT by ORDINAL1:def 12;
n to_power p > 0 by POWER:34,A19;
then 1/n to_power p > 0;
then
A21: s1.n>0 by A15,A20;
A22: n/(n+1)<=1 by NAT_1:11,XREAL_1:183;
A23: n/(n+1)>0 by A19;
s1.(n+1)/s1.n = (1/(n+1) to_power p)/s1.n by A15
.= (1/(n+1) to_power p)/(1/n to_power p) by A15,A19
.= (1/(n+1) to_power p) * n to_power p
.= n to_power p / (n+1) to_power p
.= (n/(n+1)) to_power p by A19,POWER:31
.= (n/(n+1)) #R p by A23,POWER:def 2;
then s1.(n+1)/s1.n <= (n/(n+1)) #R 0 by A10,A23,A22,PREPOWER:84;
then s1.(n+1)/s1.n <= 1 by A19,PREPOWER:71;
hence s1.(n+1)<=s1 .n by A21,XREAL_1:187;
end;
end;
hence s1.(n+1)<=s1.n;
end;
then
A24: s1 is non-increasing;
A25: now
let n;
A26: n in NAT by ORDINAL1:def 12;
assume
A27: n>=1;
then s.n = 1/n to_power p by A2
.= s1.n by A15,A27,A26;
hence s.n>=s1.n;
end;
deffunc U(Nat) = 2 to_power $1 * s1.(2 to_power $1);
consider s2 such that
A28: for n holds s2.n = U(n) from SEQ_1:sch 1;
A29: now
let n;
now
per cases by NAT_1:6;
suppose
n=0;
hence s1.n >= 0 by A15;
end;
suppose
A30: ex m be Nat st n=m+1;
A31: n in NAT by ORDINAL1:def 12;
n to_power p > 0 by POWER:34,A30;
then 1/n to_power p >= 0;
hence s1.n>=0 by A15,A31;
end;
end;
hence s1.n>=0 & s2.n = 2 to_power n * s1.(2 to_power n) by A28;
end;
now
assume s2 is convergent & lim s2=0;
then consider m such that
A32: for n st n>=m holds |.s2.n-0.|<1/2 by SEQ_2:def 7;
now
let n;
assume n>=m;
then |.s2.n-0.|<1/2 by A32;
then
A33: |.2 to_power n * s1.(2 to_power n).|<1/2 by A28;
2 to_power n >= 1 by PREPOWER:11;
then |.2 to_power n * (1/(2 to_power n) to_power p).|<1/2 by A15,A33;
then |.2 to_power n * (1/2 to_power (n*p)).|<1/2 by POWER:33;
then |.2 to_power n * 2 to_power (-n*p).|<1/2 by POWER:28;
then |.2 to_power (n+-n*p).|<1/2 by POWER:27;
then 2 to_power (n-n*p)<1/2 by ABSVALUE:def 1;
then 2 to_power (n-n*p)*2<1/2*2 by XREAL_1:68;
then 2 to_power (n-n*p)*2 to_power 1<1;
then
A34: 2 to_power (n-n*p+1)<1 by POWER:27;
1-p>=0 by A1,XREAL_1:48;
then n*(1-p)>=0;
then 2 #R (n-n*p+1) >= 1 by PREPOWER:85;
hence contradiction by A34,POWER:def 2;
end;
hence contradiction;
end;
then not s2 is summable by Th4;
then not s1 is summable by A24,A29,Th31;
hence thesis by A29,A25,Th19;
end;
end;
definition
let s;
attr s is absolutely_summable means
abs s is summable;
end;
theorem Th34:
for n,m st n<=m holds |.Partial_Sums(s).m - Partial_Sums(s).n.|
<= |.Partial_Sums(|.s.|).m - Partial_Sums(|.s.|).n.|
proof
let n,m such that
A1: n<=m;
reconsider u=n, v=m as Integer;
set s2=Partial_Sums(abs(s));
set s1=Partial_Sums(s);
defpred X[Nat] means
|.s1.(n+$1) - s1.n.| <= |.s2.(n+$1) - s2.n.|;
now
let k;
|.s.k.|>=0 by COMPLEX1:46;
hence abs(s).k >= 0 by SEQ_1:12;
end;
then
A2: s2 is non-decreasing by Th16;
A3: for k st X[k] holds X[k+1]
proof
let k;
A4: |.s.(n+k+1).| >= 0 by COMPLEX1:46;
assume |.s1.(n+k) - s1.n.| <= |.s2.(n+k) - s2.n.|;
then
A5: |.s.(n+k+1).| + |.s1.(n+k) - s1.n.| <= |.s.(n+k+1).| + |.s2.(n+k
) - s2.n.| by XREAL_1:7;
A6: |.s2.(n+(k+1)) - s2.n.| = |.s2.(n+k) + (abs(s)).(n+k+1) - s2.n.| by Def1
.= |.|.s.(n+k+1).| + s2.(n+k) - s2.n.| by SEQ_1:12
.= |.|.s.(n+k+1).| + (s2.(n+k) - s2.n).|;
s2.(n+k)>=s2.n by A2,SEQM_3:5;
then
A7: s2.(n+k) - s2.n >= 0 by XREAL_1:48;
|.s1.(n+(k+1)) - s1.n.| = |.s.(n+k+1) + s1.(n+k) - s1.n.| by Def1
.= |.s.(n+k+1) + (s1.(n+k) - s1.n).|;
then |.s1.(n+(k+1))-s1.n.| <= |.s.(n+k+1).|+|.s1.(n+k) - s1.n.| by
COMPLEX1:56;
then |.s1.(n+(k+1))-s1.n.| <= |.s.(n+k+1).|+|.s2.(n+k)-s2.n.| by A5,
XXREAL_0:2;
then |.s1.(n+(k+1))-s1.n.| <= |.s.(n+k+1).|+(s2.(n+k)-s2.n) by A7,
ABSVALUE:def 1;
hence thesis by A7,A4,A6,ABSVALUE:def 1;
end;
reconsider k = v-u as Element of NAT by A1,INT_1:5;
A8: n+k = m;
A9: X[0];
for k holds X[k] from NAT_1:sch 2(A9,A3);
hence thesis by A8;
end;
registration
cluster absolutely_summable -> summable for Real_Sequence;
coherence
proof let s be Real_Sequence;
assume s is absolutely_summable;
then
A1: abs s is summable;
now
let r;
assume 0<r;
then consider n such that
A2: for m st n<=m holds |.Partial_Sums(abs(s)).m - Partial_Sums(abs(
s)).n.|<r by A1,Th21;
take n;
let m;
assume
A3: n<=m;
then
A4: |.Partial_Sums(s).m - Partial_Sums(s).n.| <= |.Partial_Sums(abs(s))
.m - Partial_Sums(abs(s)).n.| by Th34;
|.Partial_Sums(abs(s)).m - Partial_Sums(abs(s)).n.|<r by A2,A3;
hence |. Partial_Sums(s).m - Partial_Sums(s).n.|<r by A4,XXREAL_0:2;
end;
hence thesis by Th21;
end;
end;
theorem
s is absolutely_summable implies s is summable;
theorem
(for n holds 0<=s.n) & s is summable implies s is absolutely_summable
proof
assume that
A1: for n holds 0<=s.n and
A2: s is summable;
A3: for n holds s.n = |.s.n.| by A1,ABSVALUE:def 1;
Partial_Sums(s) is convergent by A2;
then Partial_Sums(abs(s)) is convergent by A3,SEQ_1:12;
then abs(s) is summable;
hence thesis;
end;
theorem
(for n holds s.n<>0 & s1.n=abs(s).(n+1)/abs(s).n) & s1 is convergent &
lim s1 < 1 implies s is absolutely_summable
proof
assume that
A1: for n holds s.n<>0 & s1.n=abs(s).(n+1)/abs(s).n and
A2: s1 is convergent & lim s1 < 1;
now
let n;
abs(s).n = |.s.n.| & s.n <> 0 by A1,SEQ_1:12;
hence abs(s).n > 0 by COMPLEX1:47;
thus s1.n=abs(s).(n+1)/abs(s).n by A1;
end;
then abs(s) is summable by A2,Th26;
hence thesis;
end;
theorem Th38:
r>0 & (ex m st for n st n>=m holds |.s.n.|>=r) implies s is not
convergent or lim s <> 0
proof
assume
A1: r>0;
given m such that
A2: for n st n>=m holds |.s.n.|>=r;
now
per cases;
suppose
s is not convergent;
hence thesis;
end;
suppose
A3: s is convergent;
now
assume lim s=0;
then consider k such that
A4: for n st n>=k holds |.s.n-0.|<r by A1,A3,SEQ_2:def 7;
now
let n such that
A5: n>=m+k;
m+k>=k by NAT_1:11;
then n>=k by A5,XXREAL_0:2;
then
A6: |.s.n-0.|<r by A4;
m+k>=m by NAT_1:11;
then n>=m by A5,XXREAL_0:2;
hence contradiction by A2,A6;
end;
hence contradiction;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
(for n holds s.n<>0) & (ex m st for n st n>=m holds abs(s).(n+1)/abs(s
).n >= 1) implies s is not summable
proof
assume
A1: for n holds s.n<>0;
given m such that
A2: for n st n>=m holds abs(s).(n+1)/abs(s).n >= 1;
A3: now
defpred X[Nat] means |.s.(m+$1).|>=|.s.m.|;
A4: for k st X[k] holds X[k+1]
proof
let k such that
A5: |.s.(m+k).|>=|.s.m.|;
abs(s).(m+k+1)/abs(s).(m+k) >= 1 by A2,NAT_1:11;
then |.s.(m+k+1).|/abs(s).(m+k) >= 1 by SEQ_1:12;
then
A6: |.s.(m+k+1).|/|.s.(m+k).| >= 1 by SEQ_1:12;
s.(m+k) <> 0 by A1;
then |.s.(m+k).| > 0 by COMPLEX1:47;
then |.s.(m+k+1).|>=|.s.(m+k).| by A6,XREAL_1:191;
hence thesis by A5,XXREAL_0:2;
end;
let n;
assume n>=m;
then consider k be Nat such that
A7: n=m+k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
A8: n=m+k by A7;
A9: X[0];
for k holds X[k] from NAT_1:sch 2(A9,A4);
hence |.s.n.|>=|.s.m.| by A8;
end;
s.m <> 0 by A1;
then |.s.m.| > 0 by COMPLEX1:47;
then s is not convergent or lim s <> 0 by A3,Th38;
hence thesis by Th4;
end;
theorem
(for n holds s1.n = n-root (abs(s).n)) & s1 is convergent & lim s1 < 1
implies s is absolutely_summable
proof
assume that
A1: for n holds s1.n = n-root (abs(s).n) and
A2: s1 is convergent & lim s1 < 1;
now
let n;
abs(s).n = |.s.n.| by SEQ_1:12;
hence abs(s).n >= 0 by COMPLEX1:46;
thus s1.n = n-root (abs(s).n) by A1;
end;
then abs(s) is summable by A2,Th28;
hence thesis;
end;
theorem
(for n holds s1.n = n-root(abs(s).n)) & (ex m st for n st m<=n holds
s1.n >= 1 ) implies s is not summable
proof
assume
A1: for n holds s1.n = n-root (abs(s).n);
given m such that
A2: for n st m<=n holds s1.n>=1;
now
let n such that
A3: n>=m+1;
m+1>=1 by NAT_1:11;
then
A4: n>=1 by A3,XXREAL_0:2;
m+1>=m by NAT_1:11;
then
A5: n>=m by A3,XXREAL_0:2;
s1.n = n-root (abs(s).n) by A1
.= n-root |.s.n.| by SEQ_1:12;
then |.s.n.| >= 0 & n-root |.s.n.| |^ n >= 1 by A2,A5,COMPLEX1:46
,PREPOWER:11;
hence |.s.n.| >= 1 by A4,POWER:4;
end;
then s is not convergent or lim s<>0 by Th38;
hence thesis by Th4;
end;
theorem
(for n holds s1.n = n-root (abs(s).n)) & s1 is convergent & lim s1 > 1
implies s is not summable
proof
assume that
A1: for n holds s1.n = n-root (abs(s).n) and
A2: s1 is convergent and
A3: lim s1 > 1;
lim s1 - 1 > 0 by A3,XREAL_1:50;
then consider m such that
A4: for n st n>=m holds |.s1.n-lim s1.|<lim s1-1 by A2,SEQ_2:def 7;
now
let n such that
A5: n>=m+1;
A6: s1.n = n-root (abs(s).n) by A1
.= n-root |.s.n.| by SEQ_1:12;
m+1>=m by NAT_1:11;
then n>=m by A5,XXREAL_0:2;
then |.n-root |.s.n.| - lim s1.| < lim s1 - 1 by A4,A6;
then -(lim s1 - 1) < n-root |.s.n.| - lim s1 by SEQ_2:1;
then 1 - lim s1 + lim s1 < n-root |.s.n.| - lim s1 + lim s1 by XREAL_1:6;
then
A7: |.s.n.| >= 0 & n-root |.s.n.| |^ n >= 1 by COMPLEX1:46,PREPOWER:11;
m+1>=1 by NAT_1:11;
then n>=1 by A5,XXREAL_0:2;
hence |.s.n.| >= 1 by A7,POWER:4;
end;
then s is not convergent or lim s<>0 by Th38;
hence thesis by Th4;
end;
begin :: Addenda
:: from BHSP_4, 2006.03.04, A.T.
definition
let s;
let n be Nat;
func Sum(s, n) -> Real equals
Partial_Sums(s).n;
coherence;
end;
definition
let s;
let n,m be Nat;
func Sum(s, n, m) -> Real equals
Sum(s, n) - Sum(s, m);
coherence;
end;