:: SERIES_1 semantic presentation
begin
theorem Th1: :: SERIES_1:1
for a being real number
for s being Real_Sequence st 0 < a & a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) holds
( s is convergent & lim s = 0 )
proof
let a be real number ; ::_thesis: for s being Real_Sequence st 0 < a & a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) holds
( s is convergent & lim s = 0 )
let s be Real_Sequence; ::_thesis: ( 0 < a & a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) implies ( s is convergent & lim s = 0 ) )
assume that
A1: 0 < a and
A2: a < 1 and
A3: for n being Element of NAT holds s . n = a to_power (n + 1) ; ::_thesis: ( s is convergent & lim s = 0 )
set r = (1 / a) - 1;
1 / a > 1 / 1 by A1, A2, XREAL_1:88;
then A4: (1 / a) - 1 > 0 by XREAL_1:50;
A5: for p being real number st 0 < p holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p
proof
let p be real number ; ::_thesis: ( 0 < p implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p )
A6: 1 / (p * ((1 / a) - 1)) <= [\(1 / (p * ((1 / a) - 1)))/] + 1 by INT_1:29;
assume A7: 0 < p ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p
then p * ((1 / a) - 1) > 0 by A4;
then 1 / (p * ((1 / a) - 1)) > 0 ;
then [\(1 / (p * ((1 / a) - 1)))/] is Element of NAT by A6, INT_1:3, INT_1:7;
then consider m being Element of NAT such that
A8: m = [\(1 / (p * ((1 / a) - 1)))/] ;
take m ; ::_thesis: for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p
A9: 1 / (p * ((1 / a) - 1)) = (1 / p) / ((1 / a) - 1) by XCMPLX_1:78;
now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
abs_((s_._n)_-_0)_<_p
A10: [\(1 / (p * ((1 / a) - 1)))/] > (1 / (p * ((1 / a) - 1))) - 1 by INT_1:def_6;
let n be Element of NAT ; ::_thesis: ( m <= n implies abs ((s . n) - 0) < p )
assume m <= n ; ::_thesis: abs ((s . n) - 0) < p
then n > (1 / (p * ((1 / a) - 1))) - 1 by A8, A10, XXREAL_0:2;
then n + 1 > (1 / p) / ((1 / a) - 1) by A9, XREAL_1:19;
then A11: (n + 1) * ((1 / a) - 1) > 1 / p by A4, XREAL_1:77;
0 + ((n + 1) * ((1 / a) - 1)) < 1 + ((n + 1) * ((1 / a) - 1)) by XREAL_1:6;
then A12: 1 / p < 1 + ((n + 1) * ((1 / a) - 1)) by A11, XXREAL_0:2;
A13: (1 + ((1 / a) - 1)) to_power (n + 1) = (1 to_power (n + 1)) / (a to_power (n + 1)) by A1, POWER:31
.= 1 / (a to_power (n + 1)) by POWER:26 ;
a to_power (n + 1) > 0 by A1, POWER:34;
then A14: abs (a to_power (n + 1)) = a to_power (n + 1) by ABSVALUE:def_1;
1 + ((n + 1) * ((1 / a) - 1)) <= (1 + ((1 / a) - 1)) to_power (n + 1) by A4, POWER:49;
then 1 / p < 1 / (a to_power (n + 1)) by A13, A12, XXREAL_0:2;
then abs (a to_power (n + 1)) < p by A7, A14, XREAL_1:91;
hence abs ((s . n) - 0) < p by A3; ::_thesis: verum
end;
hence for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p ; ::_thesis: verum
end;
hence s is convergent by SEQ_2:def_6; ::_thesis: lim s = 0
hence lim s = 0 by A5, SEQ_2:def_7; ::_thesis: verum
end;
theorem Th2: :: SERIES_1:2
for a being real number
for n being Nat holds (abs a) to_power n = abs (a to_power n)
proof
let a be real number ; ::_thesis: for n being Nat holds (abs a) to_power n = abs (a to_power n)
let n be Nat; ::_thesis: (abs a) to_power n = abs (a to_power n)
percases ( a <> 0 or a = 0 ) ;
supposeA1: a <> 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n)
then A2: abs a > 0 by COMPLEX1:47;
now__::_thesis:_(abs_a)_to_power_n_=_abs_(a_to_power_n)
percases ( a > 0 or a < 0 ) by A1;
suppose a > 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n)
then ( a to_power n = (abs a) to_power n & a to_power n > 0 ) by ABSVALUE:def_1, POWER:34;
hence (abs a) to_power n = abs (a to_power n) by ABSVALUE:def_1; ::_thesis: verum
end;
supposeA3: a < 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n)
reconsider m = n as Integer ;
now__::_thesis:_(abs_a)_to_power_n_=_abs_(a_to_power_n)
percases ( m is even or m is odd ) ;
supposeA4: m is even ; ::_thesis: (abs a) to_power n = abs (a to_power n)
A5: (abs a) to_power n > 0 by A2, POWER:34;
(abs a) to_power n = (- a) to_power m by A3, ABSVALUE:def_1
.= a to_power m by A4, POWER:47 ;
hence (abs a) to_power n = abs (a to_power n) by A5, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA6: m is odd ; ::_thesis: (abs a) to_power n = abs (a to_power n)
A7: (abs a) to_power n > 0 by A2, POWER:34;
(abs a) to_power n = (- a) to_power m by A3, ABSVALUE:def_1
.= - (a to_power m) by A6, POWER:48 ;
hence (abs a) to_power n = abs (- (a to_power n)) by A7, ABSVALUE:def_1
.= abs (a to_power n) by COMPLEX1:52 ;
::_thesis: verum
end;
end;
end;
hence (abs a) to_power n = abs (a to_power n) ; ::_thesis: verum
end;
end;
end;
hence (abs a) to_power n = abs (a to_power n) ; ::_thesis: verum
end;
supposeA8: a = 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n)
percases ( n = 0 or n > 0 ) ;
suppose n = 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n)
then a to_power n = 1 by NEWTON:4;
hence (abs a) to_power n = abs (a to_power n) by A8, COMPLEX1:44, COMPLEX1:48; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n)
then (abs a) to_power n = 0 by A8, COMPLEX1:44, POWER:def_2;
hence (abs a) to_power n = abs (a to_power n) by A8, COMPLEX1:44; ::_thesis: verum
end;
end;
end;
end;
end;
theorem Th3: :: SERIES_1:3
for a being real number
for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) holds
( s is convergent & lim s = 0 )
proof
let a be real number ; ::_thesis: for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) holds
( s is convergent & lim s = 0 )
let s be Real_Sequence; ::_thesis: ( abs a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) implies ( s is convergent & lim s = 0 ) )
assume that
A1: abs a < 1 and
A2: for n being Element of NAT holds s . n = a to_power (n + 1) ; ::_thesis: ( s is convergent & lim s = 0 )
now__::_thesis:_(_s_is_convergent_&_lim_s_=_0_)
percases ( abs a = 0 or not abs a = 0 ) ;
suppose abs a = 0 ; ::_thesis: ( s is convergent & lim s = 0 )
then A3: a = 0 by ABSVALUE:2;
now__::_thesis:_for_n_being_Nat_holds_s_._n_=_0
let n be Nat; ::_thesis: s . n = 0
( n in NAT & a to_power (n + 1) = 0 ) by A3, ORDINAL1:def_12, POWER:def_2;
hence s . n = 0 by A2; ::_thesis: verum
end;
then ( s is constant & s . 0 = 0 ) by VALUED_0:def_18;
hence ( s is convergent & lim s = 0 ) by SEQ_4:26; ::_thesis: verum
end;
supposeA4: not abs a = 0 ; ::_thesis: ( s is convergent & lim s = 0 )
deffunc H1( Element of NAT ) -> Element of REAL = (abs a) to_power ($1 + 1);
consider s1 being Real_Sequence such that
A5: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_=_abs_(s_._n)
let n be Element of NAT ; ::_thesis: s1 . n = abs (s . n)
thus s1 . n = (abs a) to_power (n + 1) by A5
.= abs (a to_power (n + 1)) by Th2
.= abs (s . n) by A2 ; ::_thesis: verum
end;
A7: abs 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 ( s is convergent & lim s = 0 ) by A8, SEQ_4:15; ::_thesis: verum
end;
end;
end;
hence ( s is convergent & lim s = 0 ) ; ::_thesis: verum
end;
definition
let X be non empty complex-membered add-closed set ;
let s1, s2 be sequence of X;
:: original: +
redefine funcs1 + s2 -> sequence of X;
coherence
s1 + s2 is sequence of X
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__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
(s1_+_s2)_._x_in_X
let x be set ; ::_thesis: ( x in NAT implies (s1 + s2) . x in X )
assume A2: x in NAT ; ::_thesis: (s1 + s2) . x in X
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; ::_thesis: verum
end;
hence s1 + s2 is sequence of X by A1, FUNCT_2:3; ::_thesis: verum
end;
end;
definition
let s be complex-valued ManySortedSet of NAT ;
func Partial_Sums s -> complex-valued ManySortedSet of NAT means :Def1: :: SERIES_1:def 1
( it . 0 = s . 0 & ( for n being Element of NAT holds it . (n + 1) = (it . n) + (s . (n + 1)) ) );
existence
ex b1 being complex-valued ManySortedSet of NAT st
( b1 . 0 = s . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) )
proof
set X = COMPLEX ;
A1: dom s = NAT by PARTFUN1:def_2;
rng s c= COMPLEX by VALUED_0:def_1;
then reconsider ss = s as Function of NAT,COMPLEX by A1, RELSET_1:4;
defpred S1[ Nat, Element of COMPLEX , set ] means $3 = $2 + (ss . ($1 + 1));
A2: for n being Element of NAT
for x being Element of COMPLEX ex y being Element of COMPLEX st S1[n,x,y] ;
ex f being Function of NAT,COMPLEX st
( f . 0 = ss . 0 & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A2);
hence ex b1 being complex-valued ManySortedSet of NAT st
( b1 . 0 = s . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being complex-valued ManySortedSet of NAT st b1 . 0 = s . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) & b2 . 0 = s . 0 & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) + (s . (n + 1)) ) holds
b1 = b2
proof
let s1, s2 be complex-valued ManySortedSet of NAT ; ::_thesis: ( s1 . 0 = s . 0 & ( for n being Element of NAT holds s1 . (n + 1) = (s1 . n) + (s . (n + 1)) ) & s2 . 0 = s . 0 & ( for n being Element of NAT holds s2 . (n + 1) = (s2 . n) + (s . (n + 1)) ) implies s1 = s2 )
assume that
A3: s1 . 0 = s . 0 and
A4: for n being Element of NAT holds s1 . (n + 1) = (s1 . n) + (s . (n + 1)) and
A5: s2 . 0 = s . 0 and
A6: for n being Element of NAT holds s2 . (n + 1) = (s2 . n) + (s . (n + 1)) ; ::_thesis: s1 = s2
defpred S1[ Element of NAT ] means s1 . $1 = s2 . $1;
A7: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume s1 . k = s2 . k ; ::_thesis: S1[k + 1]
hence s1 . (k + 1) = (s2 . k) + (s . (k + 1)) by A4
.= s2 . (k + 1) by A6 ;
::_thesis: verum
end;
A8: S1[ 0 ] by A3, A5;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A7); :: according to PBOOLE:def_21 ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Partial_Sums SERIES_1:def_1_:_
for s, b2 being complex-valued ManySortedSet of NAT holds
( b2 = Partial_Sums s iff ( b2 . 0 = s . 0 & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) + (s . (n + 1)) ) ) );
registration
let s be real-valued ManySortedSet of NAT ;
cluster Partial_Sums s -> complex-valued real-valued ;
coherence
Partial_Sums s is real-valued
proof
set f = Partial_Sums s;
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (Partial_Sums s) or (Partial_Sums s) . x is real )
assume x in dom (Partial_Sums s) ; ::_thesis: (Partial_Sums s) . x is real
then reconsider n = x as Element of NAT ;
defpred S1[ Nat] means (Partial_Sums s) . s is real ;
(Partial_Sums s) . 0 = s . 0 by Def1;
then A1: S1[ 0 ] ;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def_12;
(Partial_Sums s) . (k + 1) = ((Partial_Sums s) . k) + (s . (k + 1)) by Def1;
hence S1[k + 1] by A3; ::_thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2);
then (Partial_Sums s) . n is real ;
hence (Partial_Sums s) . x is real ; ::_thesis: verum
end;
end;
definition
let s be Real_Sequence;
:: original: Partial_Sums
redefine func Partial_Sums s -> Real_Sequence;
coherence
Partial_Sums s is Real_Sequence
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 ; ::_thesis: verum
end;
end;
definition
let s be Real_Sequence;
attrs is summable means :Def2: :: SERIES_1:def 2
Partial_Sums s is convergent ;
func Sum s -> Real equals :: SERIES_1:def 3
lim (Partial_Sums s);
correctness
coherence
lim (Partial_Sums s) is Real;
;
end;
:: deftheorem Def2 defines summable SERIES_1:def_2_:_
for s being Real_Sequence holds
( s is summable iff Partial_Sums s is convergent );
:: deftheorem defines Sum SERIES_1:def_3_:_
for s being Real_Sequence holds Sum s = lim (Partial_Sums s);
theorem Th4: :: SERIES_1:4
for s being Real_Sequence st s is summable holds
( s is convergent & lim s = 0 )
proof
let s be Real_Sequence; ::_thesis: ( s is summable implies ( s is convergent & lim s = 0 ) )
assume s is summable ; ::_thesis: ( s is convergent & lim s = 0 )
then A1: Partial_Sums s is convergent by Def2;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_s)_^\_1)_._n_=_((Partial_Sums_s)_._n)_+_((s_^\_1)_._n)
let n be Element of NAT ; ::_thesis: ((Partial_Sums s) ^\ 1) . n = ((Partial_Sums s) . n) + ((s ^\ 1) . 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; ::_thesis: verum
end;
then A2: (Partial_Sums s) ^\ 1 = (Partial_Sums s) + (s ^\ 1) by SEQ_1:7;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((s_^\_1)_+_((Partial_Sums_s)_-_(Partial_Sums_s)))_._n_=_(s_^\_1)_._n
let n be Element of NAT ; ::_thesis: ((s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s))) . n = (s ^\ 1) . n
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 ; ::_thesis: verum
end;
then (s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s)) = s ^\ 1 by FUNCT_2:63;
then A3: s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s) by A2, SEQ_1:31;
then A4: s ^\ 1 is convergent by A1;
hence s is convergent by SEQ_4:21; ::_thesis: lim s = 0
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 lim s = 0 by A3, A4, SEQ_4:22; ::_thesis: verum
end;
Lm1: for seq, seq1, seq2 being complex-valued ManySortedSet of NAT holds
( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) )
proof
let seq, seq1, seq2 be complex-valued ManySortedSet of NAT ; ::_thesis: ( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) )
thus ( seq = seq1 + seq2 implies for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) ::_thesis: ( ( for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) implies seq = seq1 + seq2 )
proof
assume A1: seq = seq1 + seq2 ; ::_thesis: for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n)
let n be Element of NAT ; ::_thesis: seq . n = (seq1 . n) + (seq2 . n)
dom seq = NAT by PARTFUN1:def_2;
hence seq . n = (seq1 . n) + (seq2 . n) by A1, VALUED_1:def_1; ::_thesis: verum
end;
assume for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ; ::_thesis: seq = seq1 + seq2
then A2: for n being set 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 seq = seq1 + seq2 by A2, VALUED_1:def_1; ::_thesis: verum
end;
theorem Th5: :: SERIES_1:5
for X being non empty complex-membered add-closed 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 complex-membered add-closed set ; ::_thesis: for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)
let s1, s2 be sequence of X; ::_thesis: (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)
A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_s1)_+_(Partial_Sums_s2))_._(n_+_1)_=_(((Partial_Sums_s1)_+_(Partial_Sums_s2))_._n)_+_((s1_+_s2)_._(n_+_1))
let n be Element of NAT ; ::_thesis: ((Partial_Sums s1) + (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) + (Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1))
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 ; ::_thesis: verum
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 (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) by A1, Def1; ::_thesis: verum
end;
theorem Th6: :: SERIES_1:6
for s1, s2 being Real_Sequence holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)
proof
let s1, s2 be Real_Sequence; ::_thesis: (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)
A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_s1)_-_(Partial_Sums_s2))_._(n_+_1)_=_(((Partial_Sums_s1)_-_(Partial_Sums_s2))_._n)_+_((s1_-_s2)_._(n_+_1))
let n be Element of NAT ; ::_thesis: ((Partial_Sums s1) - (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) - (Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1))
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 ; ::_thesis: verum
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 (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) by A1, Def1; ::_thesis: verum
end;
theorem :: SERIES_1:7
for s1, s2 being Real_Sequence st s1 is summable & s2 is summable holds
( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) )
proof
let s1, s2 be Real_Sequence; ::_thesis: ( s1 is summable & s2 is summable implies ( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) ) )
assume ( s1 is summable & s2 is summable ) ; ::_thesis: ( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) )
then A1: ( Partial_Sums s1 is convergent & Partial_Sums s2 is convergent ) by Def2;
then (Partial_Sums s1) + (Partial_Sums s2) is convergent ;
then Partial_Sums (s1 + s2) is convergent by Th5;
hence s1 + s2 is summable by Def2; ::_thesis: Sum (s1 + s2) = (Sum s1) + (Sum s2)
thus Sum (s1 + s2) = lim ((Partial_Sums s1) + (Partial_Sums s2)) by Th5
.= (Sum s1) + (Sum s2) by A1, SEQ_2:6 ; ::_thesis: verum
end;
theorem :: SERIES_1:8
for s1, s2 being Real_Sequence st s1 is summable & s2 is summable holds
( s1 - s2 is summable & Sum (s1 - s2) = (Sum s1) - (Sum s2) )
proof
let s1, s2 be Real_Sequence; ::_thesis: ( s1 is summable & s2 is summable implies ( s1 - s2 is summable & Sum (s1 - s2) = (Sum s1) - (Sum s2) ) )
assume ( s1 is summable & s2 is summable ) ; ::_thesis: ( s1 - s2 is summable & Sum (s1 - s2) = (Sum s1) - (Sum s2) )
then A1: ( Partial_Sums s1 is convergent & Partial_Sums s2 is convergent ) by Def2;
then (Partial_Sums s1) - (Partial_Sums s2) is convergent ;
then Partial_Sums (s1 - s2) is convergent by Th6;
hence s1 - s2 is summable by Def2; ::_thesis: Sum (s1 - s2) = (Sum s1) - (Sum s2)
thus Sum (s1 - s2) = lim ((Partial_Sums s1) - (Partial_Sums s2)) by Th6
.= (Sum s1) - (Sum s2) by A1, SEQ_2:12 ; ::_thesis: verum
end;
theorem Th9: :: SERIES_1:9
for r being real number
for s being Real_Sequence holds Partial_Sums (r (#) s) = r (#) (Partial_Sums s)
proof
let r be real number ; ::_thesis: for s being Real_Sequence holds Partial_Sums (r (#) s) = r (#) (Partial_Sums s)
let s be Real_Sequence; ::_thesis: Partial_Sums (r (#) s) = r (#) (Partial_Sums s)
A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(Partial_Sums_s))_._(n_+_1)_=_((r_(#)_(Partial_Sums_s))_._n)_+_((r_(#)_s)_._(n_+_1))
let n be Element of NAT ; ::_thesis: (r (#) (Partial_Sums s)) . (n + 1) = ((r (#) (Partial_Sums s)) . n) + ((r (#) s) . (n + 1))
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 ; ::_thesis: verum
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 Partial_Sums (r (#) s) = r (#) (Partial_Sums s) by A1, Def1; ::_thesis: verum
end;
theorem Th10: :: SERIES_1:10
for r being real number
for s being Real_Sequence st s is summable holds
( r (#) s is summable & Sum (r (#) s) = r * (Sum s) )
proof
let r be real number ; ::_thesis: for s being Real_Sequence st s is summable holds
( r (#) s is summable & Sum (r (#) s) = r * (Sum s) )
let s be Real_Sequence; ::_thesis: ( s is summable implies ( r (#) s is summable & Sum (r (#) s) = r * (Sum s) ) )
assume s is summable ; ::_thesis: ( r (#) s is summable & Sum (r (#) s) = r * (Sum s) )
then A1: Partial_Sums s is convergent by Def2;
then r (#) (Partial_Sums s) is convergent ;
then Partial_Sums (r (#) s) is convergent by Th9;
hence r (#) s is summable by Def2; ::_thesis: Sum (r (#) s) = r * (Sum s)
thus Sum (r (#) s) = lim (r (#) (Partial_Sums s)) by Th9
.= r * (Sum s) by A1, SEQ_2:8 ; ::_thesis: verum
end;
theorem Th11: :: SERIES_1:11
for s, s1 being Real_Sequence st ( for n being Element of NAT holds s1 . n = s . 0 ) holds
Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1
proof
let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n = s . 0 ) implies Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 )
assume A1: for n being Element of NAT holds s1 . n = s . 0 ; ::_thesis: Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1
A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_(((Partial_Sums_s)_^\_1)_-_s1)_._(k_+_1)_=_((((Partial_Sums_s)_^\_1)_-_s1)_._k)_+_((s_^\_1)_._(k_+_1))
let k be Element of NAT ; ::_thesis: (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1))
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 ; ::_thesis: verum
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 Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 by A2, Def1; ::_thesis: verum
end;
theorem Th12: :: SERIES_1:12
for s being Real_Sequence st s is summable holds
for n being Element of NAT holds s ^\ n is summable
proof
let s be Real_Sequence; ::_thesis: ( s is summable implies for n being Element of NAT holds s ^\ n is summable )
defpred S1[ Element of NAT ] means s ^\ $1 is summable ;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
reconsider s1 = NAT --> ((s ^\ n) . 0) as Real_Sequence ;
for k being Element of NAT holds s1 . k = (s ^\ n) . 0 by FUNCOP_1:7;
then A2: Partial_Sums ((s ^\ n) ^\ 1) = ((Partial_Sums (s ^\ n)) ^\ 1) - s1 by Th11;
assume s ^\ n is summable ; ::_thesis: S1[n + 1]
then Partial_Sums (s ^\ n) is convergent by Def2;
then ( s ^\ (n + 1) = (s ^\ n) ^\ 1 & Partial_Sums ((s ^\ n) ^\ 1) is convergent ) by A2, NAT_1:48;
hence S1[n + 1] by Def2; ::_thesis: verum
end;
assume s is summable ; ::_thesis: for n being Element of NAT holds s ^\ n is summable
then A3: S1[ 0 ] by NAT_1:47;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); ::_thesis: verum
end;
theorem Th13: :: SERIES_1:13
for s being Real_Sequence st ex n being Element of NAT st s ^\ n is summable holds
s is summable
proof
let s be Real_Sequence; ::_thesis: ( ex n being Element of NAT st s ^\ n is summable implies s is summable )
given n being Element of NAT such that A1: s ^\ n is summable ; ::_thesis: s is summable
reconsider s1 = NAT --> ((Partial_Sums s) . n) as Real_Sequence ;
for k being Element of NAT holds ((Partial_Sums s) ^\ (n + 1)) . k = ((Partial_Sums (s ^\ (n + 1))) . k) + (s1 . k)
proof
defpred S1[ Element of 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 being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: ((Partial_Sums s) ^\ (n + 1)) . k = ((Partial_Sums (s ^\ (n + 1))) . k) + (s1 . k) ; ::_thesis: S1[k + 1]
((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 FUNCOP_1:7
.= (((Partial_Sums s) ^\ (n + 1)) . k) + ((s ^\ (n + 1)) . (k + 1)) by A4, FUNCOP_1:7
.= ((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 S1[k + 1] ; ::_thesis: verum
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, FUNCOP_1:7 ;
then A5: S1[ 0 ] ;
thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A3); ::_thesis: verum
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 by Def2;
then (Partial_Sums s) ^\ (n + 1) is convergent by A6;
then Partial_Sums s is convergent by SEQ_4:21;
hence s is summable by Def2; ::_thesis: verum
end;
theorem Th14: :: SERIES_1:14
for s1, s2 being Real_Sequence st ( for n being Element of NAT holds s1 . n <= s2 . n ) holds
for n being Element of NAT holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n
proof
let s1, s2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n <= s2 . n ) implies for n being Element of NAT holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n )
defpred S1[ Element of NAT ] means (Partial_Sums s1) . $1 <= (Partial_Sums s2) . $1;
assume A1: for n being Element of NAT holds s1 . n <= s2 . n ; ::_thesis: for n being Element of NAT holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: (Partial_Sums s1) . n <= (Partial_Sums s2) . n ; ::_thesis: S1[n + 1]
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 S1[n + 1] by A3, A4, XREAL_1:7; ::_thesis: verum
end;
( (Partial_Sums s2) . 0 = s2 . 0 & (Partial_Sums s1) . 0 = s1 . 0 ) by Def1;
then A5: S1[ 0 ] by A1;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A2); ::_thesis: verum
end;
theorem :: SERIES_1:15
for s being Real_Sequence st s is summable holds
for n being Element of NAT holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1)))
proof
let s be Real_Sequence; ::_thesis: ( s is summable implies for n being Element of NAT holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1))) )
defpred S1[ Element of NAT ] means Sum s = ((Partial_Sums s) . $1) + (Sum (s ^\ ($1 + 1)));
assume A1: s is summable ; ::_thesis: for n being Element of NAT holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1)))
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1))) ; ::_thesis: S1[n + 1]
reconsider s1 = NAT --> ((s ^\ (n + 1)) . 0) as Real_Sequence ;
for k being Element of NAT holds s1 . k = (s ^\ (n + 1)) . 0 by FUNCOP_1:7;
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 by Def2;
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 FUNCOP_1:7 ;
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 S1[n + 1] ; ::_thesis: verum
end;
A6: S1[ 0 ]
proof
reconsider s1 = NAT --> (s . 0) as Real_Sequence ;
A7: Partial_Sums s is convergent by A1, Def2;
for k being Element of NAT holds s1 . k = s . 0 by FUNCOP_1:7;
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 FUNCOP_1:7 ;
then Sum s = (Sum (s ^\ 1)) + (- (- (s . 0))) ;
hence S1[ 0 ] by Def1; ::_thesis: verum
end;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A2); ::_thesis: verum
end;
theorem Th16: :: SERIES_1:16
for s being Real_Sequence st ( for n being Element of NAT holds 0 <= s . n ) holds
Partial_Sums s is V41()
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= s . n ) implies Partial_Sums s is V41() )
assume A1: for n being Element of NAT holds 0 <= s . n ; ::_thesis: Partial_Sums s is V41()
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_s)_._n_<=_(Partial_Sums_s)_._(n_+_1)
let n be Element of NAT ; ::_thesis: (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1)
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; ::_thesis: verum
end;
hence Partial_Sums s is V41() by SEQM_3:def_8; ::_thesis: verum
end;
theorem Th17: :: SERIES_1:17
for s being Real_Sequence st ( for n being Element of NAT holds 0 <= s . n ) holds
( Partial_Sums s is bounded_above iff s is summable )
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= s . n ) implies ( Partial_Sums s is bounded_above iff s is summable ) )
assume for n being Element of NAT holds 0 <= s . n ; ::_thesis: ( Partial_Sums s is bounded_above iff s is summable )
then Partial_Sums s is V41() by Th16;
hence ( Partial_Sums s is bounded_above implies s is summable ) by Def2; ::_thesis: ( s is summable implies Partial_Sums s is bounded_above )
assume s is summable ; ::_thesis: Partial_Sums s is bounded_above
then Partial_Sums s is convergent by Def2;
then Partial_Sums s is bounded ;
hence Partial_Sums s is bounded_above ; ::_thesis: verum
end;
theorem :: SERIES_1:18
for s being Real_Sequence st s is summable & ( for n being Element of NAT holds 0 <= s . n ) holds
0 <= Sum s
proof
let s be Real_Sequence; ::_thesis: ( s is summable & ( for n being Element of NAT holds 0 <= s . n ) implies 0 <= Sum s )
assume that
A1: s is summable and
A2: for n being Element of NAT holds 0 <= s . n ; ::_thesis: 0 <= Sum s
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(Partial_Sums_s)_._n
let n be Element of NAT ; ::_thesis: 0 <= (Partial_Sums s) . n
( (Partial_Sums s) . 0 <= (Partial_Sums s) . n & 0 <= s . 0 ) by A2, Th16, SEQM_3:11;
hence 0 <= (Partial_Sums s) . n by Def1; ::_thesis: verum
end;
Partial_Sums s is convergent by A1, Def2;
hence 0 <= Sum s by A3, SEQ_2:17; ::_thesis: verum
end;
theorem Th19: :: SERIES_1:19
for s2, s1 being Real_Sequence st ( for n being Element of NAT holds 0 <= s2 . n ) & s1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
s2 . n <= s1 . n holds
s2 is summable
proof
let s2, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= s2 . n ) & s1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
s2 . n <= s1 . n implies s2 is summable )
assume that
A1: for n being Element of NAT holds 0 <= s2 . n and
A2: s1 is summable ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st
( m <= n & not s2 . n <= s1 . n ) or s2 is summable )
given m being Element of NAT such that A3: for n being Element of NAT st m <= n holds
s2 . n <= s1 . n ; ::_thesis: s2 is summable
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(s1_^\_m)_._n
let n be Element of NAT ; ::_thesis: 0 <= (s1 ^\ m) . n
( (s1 ^\ m) . n = s1 . (n + m) & 0 <= s2 . (n + m) ) by A1, NAT_1:def_3;
hence 0 <= (s1 ^\ m) . n by A3, NAT_1:11; ::_thesis: verum
end;
s1 ^\ m is summable by A2, Th12;
then Partial_Sums (s1 ^\ m) is bounded_above by A4, Th17;
then consider r being real number such that
A5: for n being Element of NAT holds (Partial_Sums (s1 ^\ m)) . n < r by SEQ_2:def_3;
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_(s2_^\_m)_._n_<=_(s1_^\_m)_._n
let n be Element of NAT ; ::_thesis: (s2 ^\ m) . n <= (s1 ^\ m) . 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; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_(s2_^\_m))_._n_<_r
let n be Element of NAT ; ::_thesis: (Partial_Sums (s2 ^\ m)) . n < r
(Partial_Sums (s2 ^\ m)) . n <= (Partial_Sums (s1 ^\ m)) . n by A6, Th14;
hence (Partial_Sums (s2 ^\ m)) . n < r by A5, XXREAL_0:2; ::_thesis: verum
end;
then A7: Partial_Sums (s2 ^\ m) is bounded_above by SEQ_2:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(s2_^\_m)_._n
let n be Element of NAT ; ::_thesis: 0 <= (s2 ^\ m) . n
(s2 ^\ m) . n = s2 . (n + m) by NAT_1:def_3;
hence 0 <= (s2 ^\ m) . n by A1; ::_thesis: verum
end;
then s2 ^\ m is summable by A7, Th17;
hence s2 is summable by Th13; ::_thesis: verum
end;
theorem :: SERIES_1:20
for s1, s2 being Real_Sequence st ( for n being Element of NAT holds
( 0 <= s1 . n & s1 . n <= s2 . n ) ) & s2 is summable holds
( s1 is summable & Sum s1 <= Sum s2 )
proof
let s1, s2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds
( 0 <= s1 . n & s1 . n <= s2 . n ) ) & s2 is summable implies ( s1 is summable & Sum s1 <= Sum s2 ) )
assume that
A1: for n being Element of NAT holds
( 0 <= s1 . n & s1 . n <= s2 . n ) and
A2: s2 is summable ; ::_thesis: ( s1 is summable & Sum s1 <= Sum s2 )
for n being Element of NAT st 0 <= n holds
s1 . n <= s2 . n by A1;
hence s1 is summable by A1, A2, Th19; ::_thesis: Sum s1 <= Sum s2
then A3: Partial_Sums s1 is convergent by Def2;
( Partial_Sums s2 is convergent & ( for n being Element of NAT holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n ) ) by A1, A2, Def2, Th14;
hence Sum s1 <= Sum s2 by A3, SEQ_2:18; ::_thesis: verum
end;
theorem Th21: :: SERIES_1:21
for s being Real_Sequence holds
( s is summable iff for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r )
proof
let s be Real_Sequence; ::_thesis: ( s is summable iff for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r )
thus ( s is summable implies for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ) ::_thesis: ( ( for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ) implies s is summable )
proof
assume s is summable ; ::_thesis: for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r
then Partial_Sums s is convergent by Def2;
hence for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r by SEQ_4:41; ::_thesis: verum
end;
assume for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ; ::_thesis: s is summable
then Partial_Sums s is convergent by SEQ_4:41;
hence s is summable by Def2; ::_thesis: verum
end;
theorem Th22: :: SERIES_1:22
for n being Element of NAT
for a being real number st a <> 1 holds
(Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a)
proof
let n be Element of NAT ; ::_thesis: for a being real number st a <> 1 holds
(Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a)
let a be real number ; ::_thesis: ( a <> 1 implies (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) )
defpred S1[ Element of NAT ] means (Partial_Sums (a GeoSeq)) . $1 = (1 - (a to_power ($1 + 1))) / (1 - a);
assume a <> 1 ; ::_thesis: (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a)
then A1: 1 - a <> 0 ;
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) ; ::_thesis: S1[n + 1]
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) ;
::_thesis: verum
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) by POWER:25 ;
then A3: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
hence (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) ; ::_thesis: verum
end;
theorem :: SERIES_1:23
for a being real number
for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a)
proof
let a be real number ; ::_thesis: for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds
for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a)
let s be Real_Sequence; ::_thesis: ( a <> 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) )
assume that
A1: a <> 1 and
A2: for n being Element of NAT holds s . (n + 1) = a * (s . n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a)
defpred S1[ Element of NAT ] means s . $1 = (s . 0) * ((a GeoSeq) . $1);
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume s . n = (s . 0) * ((a GeoSeq) . n) ; ::_thesis: S1[n + 1]
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 S1[n + 1] ; ::_thesis: verum
end;
(a GeoSeq) . 0 = 1 by PREPOWER:3;
then A4: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(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__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_s)_._n_=_((s_._0)_*_(1_-_(a_to_power_(n_+_1))))_/_(1_-_a)
let n be Element of NAT ; ::_thesis: (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a)
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) ; ::_thesis: verum
end;
hence for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) ; ::_thesis: verum
end;
theorem Th24: :: SERIES_1:24
for a being real number st abs a < 1 holds
( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) )
proof
let a be real number ; ::_thesis: ( abs a < 1 implies ( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) ) )
deffunc H1( Element of NAT ) -> set = a to_power ($1 + 1);
consider s being Real_Sequence such that
A1: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1();
assume A2: abs a < 1 ; ::_thesis: ( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) )
then A3: ( s is convergent & lim s = 0 ) by A1, Th3;
A4: now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_m_holds_
abs_(((Partial_Sums_(a_GeoSeq))_._n)_-_(1_/_(1_-_a)))_<_r
a < 1 by A2, SEQ_2:1;
then A5: 1 - a > 0 by XREAL_1:50;
let r be real number ; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r )
assume r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r
then r * (1 - a) > 0 * r by A5;
then consider m being Element of NAT such that
A6: for n being Element of NAT st n >= m holds
abs ((s . n) - 0) < r * (1 - a) by A3, SEQ_2:def_7;
take m = m; ::_thesis: for n being Element of NAT st n >= m holds
abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r )
assume n >= m ; ::_thesis: abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r
then abs ((s . n) - 0) < r * (1 - a) by A6;
then abs ((a to_power (n + 1)) - 0) < r * (1 - a) by A1;
then A7: (abs (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: abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) = abs (((1 - (a to_power (n + 1))) / (1 - a)) - (1 / (1 - a))) by Th22
.= abs (((1 + (- (a to_power (n + 1)))) - 1) / (1 - a))
.= abs (- ((a to_power (n + 1)) / (1 - a)))
.= abs ((a to_power (n + 1)) / (1 - a)) by COMPLEX1:52
.= (abs (a to_power (n + 1))) / (abs (1 - a)) by COMPLEX1:67
.= (abs (a to_power (n + 1))) / (1 - a) by A5, ABSVALUE:def_1 ;
1 - a <> 0 by A2, SEQ_2:1;
hence abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r by A8, A7, XCMPLX_1:89; ::_thesis: verum
end;
then A9: Partial_Sums (a GeoSeq) is convergent by SEQ_2:def_6;
hence a GeoSeq is summable by Def2; ::_thesis: Sum (a GeoSeq) = 1 / (1 - a)
thus Sum (a GeoSeq) = 1 / (1 - a) by A4, A9, SEQ_2:def_7; ::_thesis: verum
end;
theorem :: SERIES_1:25
for a being real number
for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds
( s is summable & Sum s = (s . 0) / (1 - a) )
proof
let a be real number ; ::_thesis: for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds
( s is summable & Sum s = (s . 0) / (1 - a) )
let s be Real_Sequence; ::_thesis: ( abs a < 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) implies ( s is summable & Sum s = (s . 0) / (1 - a) ) )
assume that
A1: abs a < 1 and
A2: for n being Element of NAT holds s . (n + 1) = a * (s . n) ; ::_thesis: ( s is summable & Sum s = (s . 0) / (1 - a) )
defpred S1[ Element of NAT ] means s . $1 = (s . 0) * ((a GeoSeq) . $1);
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume s . n = (s . 0) * ((a GeoSeq) . n) ; ::_thesis: S1[n + 1]
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 S1[n + 1] ; ::_thesis: verum
end;
(a GeoSeq) . 0 = 1 by PREPOWER:3;
then A4: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(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 by Def2;
then Partial_Sums s is convergent by A5;
hence s is summable by Def2; ::_thesis: Sum s = (s . 0) / (1 - a)
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 Sum s = (s . 0) / (1 - a) ; ::_thesis: verum
end;
theorem Th26: :: SERIES_1:26
for s, s1 being Real_Sequence st ( for n being Element of NAT holds
( s . n > 0 & s1 . n = (s . (n + 1)) / (s . n) ) ) & s1 is convergent & lim s1 < 1 holds
s is summable
proof
let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds
( s . n > 0 & s1 . n = (s . (n + 1)) / (s . n) ) ) & s1 is convergent & lim s1 < 1 implies s is summable )
assume that
A1: for n being Element of NAT holds
( s . n > 0 & s1 . n = (s . (n + 1)) / (s . n) ) and
A2: s1 is convergent and
A3: lim s1 < 1 ; ::_thesis: s is summable
set r = (1 - (lim s1)) / 2;
0 + (lim s1) < 1 by A3;
then 0 < 1 - (lim s1) by XREAL_1:20;
then (1 - (lim s1)) / 2 > 0 ;
then consider m being Element of NAT such that
A4: for n being Element of NAT st m <= n holds
abs ((s1 . n) - (lim s1)) < (1 - (lim s1)) / 2 by A2, SEQ_2:def_7;
set s2 = ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq);
defpred S1[ Element of NAT ] means s . (m + $1) <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + $1);
A5: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_>=_0
let n be Element of NAT ; ::_thesis: s1 . n >= 0
( s . n > 0 & s . (n + 1) > 0 ) by A1;
then (s . (n + 1)) / (s . n) > 0 ;
hence s1 . n >= 0 by A1; ::_thesis: verum
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: ((1 - (lim s1)) / 2) + (lim s1) = 1 - ((1 - (lim s1)) / 2) ;
A9: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
set X = (s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m));
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A10: s . (m + k) <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k) ; ::_thesis: S1[k + 1]
abs ((s1 . (m + k)) - (lim s1)) < (1 - (lim s1)) / 2 by A4, NAT_1:11;
then (s1 . (m + k)) - (lim s1) < (1 - (lim s1)) / 2 by SEQ_2:1;
then A11: s1 . (m + k) <= 1 - ((1 - (lim s1)) / 2) by A8, XREAL_1:19;
(((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k) >= 0 by A1, A10;
then A12: (s1 . (m + k)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k)) <= (1 - ((1 - (lim s1)) / 2)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (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)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k)) by A10, A13, XREAL_1:64;
(1 - ((1 - (lim s1)) / 2)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k)) = (1 - ((1 - (lim s1)) / 2)) * (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * (((1 - ((1 - (lim s1)) / 2)) GeoSeq) . (m + k))) by SEQ_1:9
.= ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * ((((1 - ((1 - (lim s1)) / 2)) GeoSeq) . (m + k)) * (1 - ((1 - (lim s1)) / 2)))
.= ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * (((1 - ((1 - (lim s1)) / 2)) GeoSeq) . ((m + k) + 1)) by PREPOWER:3
.= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + (k + 1)) by SEQ_1:9 ;
hence S1[k + 1] by A14, A12, XXREAL_0:2; ::_thesis: verum
end;
(((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + 0) = ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * (((1 - ((1 - (lim s1)) / 2)) GeoSeq) . m) by SEQ_1:9
.= ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * ((1 - ((1 - (lim s1)) / 2)) |^ m) by PREPOWER:def_1
.= (s . m) * (((1 - ((1 - (lim s1)) / 2)) to_power (- m)) * ((1 - ((1 - (lim s1)) / 2)) to_power m))
.= (s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power ((- m) + m)) by A7, POWER:27, XREAL_1:50
.= (s . m) * 1 by POWER:24
.= s . (m + 0) ;
then A15: S1[ 0 ] ;
A16: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A9);
A17: now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
s_._n_<=_(((s_._m)_*_((1_-_((1_-_(lim_s1))_/_2))_to_power_(-_m)))_(#)_((1_-_((1_-_(lim_s1))_/_2))_GeoSeq))_._n
let n be Element of NAT ; ::_thesis: ( m <= n implies s . n <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . n )
assume m <= n ; ::_thesis: s . n <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . n
then consider k being Nat such that
A18: n = m + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
n = m + k by A18;
hence s . n <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . n by A16; ::_thesis: verum
end;
1 - (lim s1) <= 1 - 0 by A6, XREAL_1:6;
then 1 - (lim s1) < 2 * 2 by XXREAL_0:2;
then (1 - (lim s1)) / 2 < (2 * 2) / 2 by XREAL_1:74;
then (1 - (lim s1)) / 2 < 1 + 1 ;
then ((1 - (lim s1)) / 2) - 1 < 1 by XREAL_1:19;
then A19: - (((1 - (lim s1)) / 2) - 1) > - 1 by XREAL_1:24;
1 - (lim s1) > 0 by A3, XREAL_1:50;
then (1 - (lim s1)) / 2 > 0 ;
then 1 - ((1 - (lim s1)) / 2) < 1 - 0 by XREAL_1:10;
then abs (1 - ((1 - (lim s1)) / 2)) < 1 by A19, SEQ_2:1;
then (1 - ((1 - (lim s1)) / 2)) GeoSeq is summable by Th24;
then A20: ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq) is summable by Th10;
for n being Element of NAT holds 0 <= s . n by A1;
hence s is summable by A20, A17, Th19; ::_thesis: verum
end;
theorem :: SERIES_1:27
for s being Real_Sequence st ( for n being Element of NAT holds s . n > 0 ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(s . (n + 1)) / (s . n) >= 1 holds
not s is summable
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n > 0 ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(s . (n + 1)) / (s . n) >= 1 implies not s is summable )
assume that
A1: for n being Element of NAT holds s . n > 0 and
A2: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(s . (n + 1)) / (s . n) >= 1 ; ::_thesis: not s is summable
consider m being Element of NAT such that
A3: for n being Element of NAT st n >= m holds
(s . (n + 1)) / (s . n) >= 1 by A2;
defpred S1[ Element of NAT ] means s . (m + $1) >= s . m;
A4: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: s . (m + k) >= s . m ; ::_thesis: S1[k + 1]
( 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 S1[k + 1] by A5, XXREAL_0:2; ::_thesis: verum
end;
A6: S1[ 0 ] ;
A7: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A6, A4);
A8: for k being Element of NAT ex n being Element of NAT st
( n >= k & not abs ((s . n) - 0) < s . m )
proof
let k be Element of NAT ; ::_thesis: ex n being Element of NAT st
( n >= k & not abs ((s . n) - 0) < s . m )
take n = m + k; ::_thesis: ( n >= k & not abs ((s . n) - 0) < s . m )
s . n >= s . m by A7;
hence ( n >= k & not abs ((s . n) - 0) < s . m ) by NAT_1:11, SEQ_2:1; ::_thesis: verum
end;
s . m > 0 by A1;
then ( not lim s = 0 or not s is convergent ) by A8, SEQ_2:def_7;
hence not s is summable by Th4; ::_thesis: verum
end;
theorem Th28: :: SERIES_1:28
for s, s1 being Real_Sequence st ( for n being Element of NAT holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 < 1 holds
s is summable
proof
let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 < 1 implies s is summable )
assume that
A1: for n being Element of NAT holds
( s . n >= 0 & s1 . n = n -root (s . n) ) and
A2: s1 is convergent and
A3: lim s1 < 1 ; ::_thesis: s is summable
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_(s1_^\_1)_._n_>=_0
let n be Element of NAT ; ::_thesis: (s1 ^\ 1) . n >= 0
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; ::_thesis: verum
end;
set r = (1 - (lim s1)) / 2;
0 + (lim s1) < 1 by A3;
then 0 < 1 - (lim s1) by XREAL_1:20;
then (1 - (lim s1)) / 2 > 0 ;
then consider m being Element of NAT such that
A6: for n being Element of NAT st m <= n holds
abs ((s1 . n) - (lim s1)) < (1 - (lim s1)) / 2 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 - ((1 - (lim s1)) / 2) > 0 by XREAL_1:50;
set s2 = (1 - ((1 - (lim s1)) / 2)) GeoSeq ;
A9: ((1 - (lim s1)) / 2) + (lim s1) = 1 - ((1 - (lim s1)) / 2) ;
A10: for n being Element of NAT st m + 1 <= n holds
s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n
proof
let n be Element of NAT ; ::_thesis: ( m + 1 <= n implies s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n )
assume A11: m + 1 <= n ; ::_thesis: s . n <= (1 - ((1 - (lim s1)) / 2)) to_power 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 abs ((s1 . n) - (lim s1)) < (1 - (lim s1)) / 2 by A6;
then (s1 . n) - (lim s1) < (1 - (lim s1)) / 2 by SEQ_2:1;
then s1 . n < 1 - ((1 - (lim s1)) / 2) by A9, XREAL_1:19;
then A14: n -root (s . n) < 1 - ((1 - (lim s1)) / 2) by A1;
now__::_thesis:_s_._n_<_(1_-_((1_-_(lim_s1))_/_2))_to_power_n
percases ( s . n = 0 or s . n <> 0 ) ;
suppose s . n = 0 ; ::_thesis: s . n < (1 - ((1 - (lim s1)) / 2)) to_power n
hence s . n < (1 - ((1 - (lim s1)) / 2)) to_power n by A8, POWER:34; ::_thesis: verum
end;
suppose s . n <> 0 ; ::_thesis: s . n < (1 - ((1 - (lim s1)) / 2)) to_power n
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 - ((1 - (lim s1)) / 2)) to_power n by A11, A14, POWER:37;
hence s . n < (1 - ((1 - (lim s1)) / 2)) to_power n by A12, A13, POWER:4; ::_thesis: verum
end;
end;
end;
hence s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n ; ::_thesis: verum
end;
A15: for n being Element of NAT st m + 1 <= n holds
s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n
proof
let n be Element of NAT ; ::_thesis: ( m + 1 <= n implies s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n )
((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n = (1 - ((1 - (lim s1)) / 2)) to_power n by PREPOWER:def_1;
hence ( m + 1 <= n implies s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n ) by A10; ::_thesis: verum
end;
1 - (lim s1) <= 1 - 0 by A7, XREAL_1:6;
then 1 - (lim s1) < 2 * 2 by XXREAL_0:2;
then (1 - (lim s1)) / 2 < (2 * 2) / 2 by XREAL_1:74;
then (1 - (lim s1)) / 2 < 1 + 1 ;
then ((1 - (lim s1)) / 2) - 1 < 1 by XREAL_1:19;
then A16: - (((1 - (lim s1)) / 2) - 1) > - 1 by XREAL_1:24;
1 - (lim s1) > 0 by A3, XREAL_1:50;
then (1 - (lim s1)) / 2 > 0 ;
then 1 - ((1 - (lim s1)) / 2) < 1 - 0 by XREAL_1:10;
then abs (1 - ((1 - (lim s1)) / 2)) < 1 by A16, SEQ_2:1;
then (1 - ((1 - (lim s1)) / 2)) GeoSeq is summable by Th24;
hence s is summable by A1, A15, Th19; ::_thesis: verum
end;
theorem Th29: :: SERIES_1:29
for s, s1 being Real_Sequence st ( for n being Element of NAT holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
s1 . n >= 1 holds
not s is summable
proof
let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
s1 . n >= 1 implies not s is summable )
assume that
A1: for n being Element of NAT holds
( s . n >= 0 & s1 . n = n -root (s . n) ) and
A2: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
s1 . n >= 1 ; ::_thesis: not s is summable
consider m being Element of NAT such that
A3: for n being Element of NAT st m <= n holds
s1 . n >= 1 by A2;
A4: for n being Element of NAT st m + 1 <= n holds
s . n >= 1
proof
let n be Element of NAT ; ::_thesis: ( m + 1 <= n implies s . n >= 1 )
assume A5: m + 1 <= n ; ::_thesis: s . n >= 1
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__::_thesis:_s_._n_>=_1
percases ( n -root (s . n) = 1 or n -root (s . n) > 1 ) by A8, XXREAL_0:1;
suppose n -root (s . n) = 1 ; ::_thesis: s . n >= 1
then s . n = 1 |^ n by A6, A7, POWER:4;
hence s . n >= 1 by NEWTON:10; ::_thesis: verum
end;
suppose n -root (s . n) > 1 ; ::_thesis: s . n >= 1
then (n -root (s . n)) to_power n > 1 by A5, POWER:35;
hence s . n >= 1 by A6, A7, POWER:4; ::_thesis: verum
end;
end;
end;
hence s . n >= 1 ; ::_thesis: verum
end;
for k being Element of NAT ex n being Element of NAT st
( k <= n & not abs ((s . n) - 0) < 1 )
proof
let k be Element of NAT ; ::_thesis: ex n being Element of NAT st
( k <= n & not abs ((s . n) - 0) < 1 )
take n = (m + 1) + k; ::_thesis: ( k <= n & not abs ((s . n) - 0) < 1 )
not s . n < 1 by A4, NAT_1:11;
hence ( k <= n & not abs ((s . n) - 0) < 1 ) by NAT_1:11, SEQ_2:1; ::_thesis: verum
end;
then ( not s is convergent or not lim s = 0 ) by SEQ_2:def_7;
hence not s is summable by Th4; ::_thesis: verum
end;
theorem :: SERIES_1:30
for s, s1 being Real_Sequence st ( for n being Element of NAT holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 > 1 holds
not s is summable
proof
let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 > 1 implies not s is summable )
assume that
A1: for n being Element of NAT holds
( s . n >= 0 & s1 . n = n -root (s . n) ) and
A2: s1 is convergent and
A3: lim s1 > 1 ; ::_thesis: not s is summable
set r = (lim s1) - 1;
(lim s1) - 1 > 0 by A3, XREAL_1:50;
then consider m being Element of NAT such that
A4: for n being Element of NAT st m <= n holds
abs ((s1 . n) - (lim s1)) < (lim s1) - 1 by A2, SEQ_2:def_7;
for n being Element of NAT st m <= n holds
s1 . n >= 1
proof
let n be Element of NAT ; ::_thesis: ( m <= n implies s1 . n >= 1 )
assume m <= n ; ::_thesis: s1 . n >= 1
then abs ((s1 . n) - (lim s1)) < (lim s1) - 1 by A4;
then (s1 . n) - (lim s1) > - ((lim s1) - 1) by SEQ_2:1;
then ((s1 . n) - (lim s1)) + (lim s1) > (- ((lim s1) - 1)) + (lim s1) by XREAL_1:6;
hence s1 . n >= 1 ; ::_thesis: verum
end;
hence not s is summable by A1, Th29; ::_thesis: verum
end;
registration
let k, n be Nat;
clusterk to_power n -> natural ;
coherence
k to_power n is natural ;
end;
definition
let k, n be Nat;
:: original: to_power
redefine funck to_power n -> Element of NAT ;
coherence
k to_power n is Element of NAT by ORDINAL1:def_12;
end;
theorem Th31: :: SERIES_1:31
for s, s1 being Real_Sequence st s is V42() & ( for n being Element of NAT holds
( s . n >= 0 & s1 . n = (2 to_power n) * (s . (2 to_power n)) ) ) holds
( s is summable iff s1 is summable )
proof
let s, s1 be Real_Sequence; ::_thesis: ( s is V42() & ( for n being Element of NAT holds
( s . n >= 0 & s1 . n = (2 to_power n) * (s . (2 to_power n)) ) ) implies ( s is summable iff s1 is summable ) )
assume that
A1: s is V42() and
A2: for n being Element of NAT holds
( s . n >= 0 & s1 . n = (2 to_power n) * (s . (2 to_power n)) ) ; ::_thesis: ( s is summable iff s1 is summable )
A3: (Partial_Sums s) . (2 to_power (0 + 1)) = (Partial_Sums s) . (1 + 1) by POWER:25
.= ((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__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_>=_0
let n be Element of NAT ; ::_thesis: s1 . n >= 0
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; ::_thesis: verum
end;
thus ( s is summable implies s1 is summable ) ::_thesis: ( s1 is summable implies s is summable )
proof
defpred S1[ Element of NAT ] means (Partial_Sums s1) . $1 <= 2 * ((Partial_Sums s) . (2 to_power $1));
A5: s . 0 >= 0 by A2;
A6: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
deffunc H1( Element of NAT ) -> Element of REAL = ((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 being Element of NAT holds a . m = H1(m) from SEQ_1:sch_1();
defpred S2[ Element of NAT ] means ( $1 > 2 to_power n or $1 * (s . (2 to_power (n + 1))) <= a . $1 );
A8: for m being Element of NAT st S2[m] holds
S2[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S2[m] implies S2[m + 1] )
assume A9: ( m > 2 to_power n or m * (s . (2 to_power (n + 1))) <= a . m ) ; ::_thesis: S2[m + 1]
now__::_thesis:_S2[m_+_1]
percases ( m > 2 to_power n or m * (s . (2 to_power (n + 1))) <= a . m ) by A9;
suppose m > 2 to_power n ; ::_thesis: S2[m + 1]
hence S2[m + 1] by NAT_1:13; ::_thesis: verum
end;
supposeA10: m * (s . (2 to_power (n + 1))) <= a . m ; ::_thesis: S2[m + 1]
now__::_thesis:_S2[m_+_1]
percases ( m < 2 to_power n or m >= 2 to_power n ) ;
suppose m < 2 to_power n ; ::_thesis: S2[m + 1]
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) by POWER:25;
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 S2[m + 1] by A7; ::_thesis: verum
end;
suppose m >= 2 to_power n ; ::_thesis: S2[m + 1]
hence S2[m + 1] by NAT_1:13; ::_thesis: verum
end;
end;
end;
hence S2[m + 1] ; ::_thesis: verum
end;
end;
end;
hence S2[m + 1] ; ::_thesis: verum
end;
a . 0 = ((Partial_Sums s) . ((2 to_power n) + 0)) - ((Partial_Sums s) . (2 to_power n)) by A7
.= 0 ;
then A11: S2[ 0 ] ;
for m being Element of NAT holds S2[m] from NAT_1:sch_1(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)) by POWER:25;
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)) ; ::_thesis: S1[n + 1]
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) by POWER:25
.= 2 to_power (n + 1) by POWER:27 ;
hence S1[n + 1] by A13, A12, XXREAL_0:2; ::_thesis: verum
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 ; ::_thesis: s1 is summable
then Partial_Sums s is bounded_above by A2, Th17;
then consider r being real number such that
A16: for n being Element of NAT 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: S1[ 0 ] by A15, A17, A5, XREAL_1:7;
A19: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A18, A6);
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_s1)_._n_<_2_*_r
let n be Element of NAT ; ::_thesis: (Partial_Sums s1) . n < 2 * r
( 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; ::_thesis: verum
end;
then Partial_Sums s1 is bounded_above by SEQ_2:def_3;
hence s1 is summable by A4, Th17; ::_thesis: verum
end;
assume s1 is summable ; ::_thesis: s is summable
then Partial_Sums s1 is bounded_above by A4, Th17;
then consider r being real number such that
A20: for n being Element of NAT holds (Partial_Sums s1) . n < r by SEQ_2:def_3;
A21: 2 to_power 0 = 1 by POWER:24;
defpred S1[ Element of NAT ] means (Partial_Sums s) . (2 to_power ($1 + 1)) <= (((Partial_Sums s1) . $1) + (s . 0)) + (s . 2);
A22: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
defpred S2[ Element of 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 being Element of NAT st S2[m] holds
S2[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S2[m] implies S2[m + 1] )
(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))) ; ::_thesis: S2[m + 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 S2[m + 1] by Def1; ::_thesis: verum
end;
A25: S2[ 0 ] ;
for m being Element of NAT holds S2[m] from NAT_1:sch_1(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) ; ::_thesis: S1[n + 1]
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)) by POWER:25
.= 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 S1[n + 1] by A27, XXREAL_0:2; ::_thesis: verum
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: S1[ 0 ] by A3;
A29: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A28, A22);
A30: Partial_Sums s is V41() by A2, Th16;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_s)_._n_<_r_+_((s_._0)_+_(s_._2))
let n be Element of NAT ; ::_thesis: (Partial_Sums s) . n < r + ((s . 0) + (s . 2))
(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 by POWER:25;
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; ::_thesis: verum
end;
then Partial_Sums s is bounded_above by SEQ_2:def_3;
hence s is summable by A2, Th17; ::_thesis: verum
end;
theorem :: SERIES_1:32
for p being real number
for s being Real_Sequence st p > 1 & ( for n being Element of NAT st n >= 1 holds
s . n = 1 / (n to_power p) ) holds
s is summable
proof
let p be real number ; ::_thesis: for s being Real_Sequence st p > 1 & ( for n being Element of NAT st n >= 1 holds
s . n = 1 / (n to_power p) ) holds
s is summable
let s be Real_Sequence; ::_thesis: ( p > 1 & ( for n being Element of NAT st n >= 1 holds
s . n = 1 / (n to_power p) ) implies s is summable )
assume that
A1: p > 1 and
A2: for n being Element of NAT st n >= 1 holds
s . n = 1 / (n to_power p) ; ::_thesis: s is summable
defpred S1[ Element of NAT , real number ] means ( ( $1 = 0 & $2 = 1 ) or ( $1 >= 1 & $2 = 1 / ($1 to_power p) ) );
A3: for n being Element of NAT ex r being Real st S1[n,r]
proof
let n be Element of NAT ; ::_thesis: ex r being Real st S1[n,r]
( n = 0 or n >= 1 )
proof
assume that
A4: n <> 0 and
A5: n < 1 ; ::_thesis: contradiction
n >= 0 + 1 by A4, NAT_1:13;
hence contradiction by A5; ::_thesis: verum
end;
hence ex r being Real st S1[n,r] ; ::_thesis: verum
end;
consider s1 being Real_Sequence such that
A6: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A3);
deffunc H1( Element of NAT ) -> Element of REAL = (2 to_power $1) * (s1 . (2 to_power $1));
consider s2 being Real_Sequence such that
A7: for n being Element of NAT holds s2 . n = H1(n) from SEQ_1:sch_1();
A8: s1 . 0 = 1 by A6;
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._(n_+_1)_<=_s1_._n
let n be Element of NAT ; ::_thesis: s1 . (n + 1) <= s1 . n
now__::_thesis:_s1_._(n_+_1)_<=_s1_._n
percases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;
supposeA9: n = 0 ; ::_thesis: s1 . (n + 1) <= s1 . n
then (n + 1) #R p >= 1 by A1, PREPOWER:85;
then A10: (n + 1) to_power p >= 1 by POWER:def_2;
s1 . (n + 1) = 1 / ((n + 1) to_power p) by A6;
hence s1 . (n + 1) <= s1 . n by A8, A9, A10, XREAL_1:211; ::_thesis: verum
end;
supposeA11: ex m being Nat st n = m + 1 ; ::_thesis: s1 . (n + 1) <= s1 . n
then n to_power p > 0 by POWER:34;
then 1 / (n to_power p) > 0 ;
then A12: s1 . n > 0 by A6;
A13: n / (n + 1) <= 1 by NAT_1:11, XREAL_1:183;
A14: n / (n + 1) > 0 by A11;
(s1 . (n + 1)) / (s1 . n) = (1 / ((n + 1) to_power p)) / (s1 . n) by A6
.= (1 / ((n + 1) to_power p)) / (1 / (n to_power p)) by A6, A11
.= (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 A11, POWER:31
.= (n / (n + 1)) #R p by A14, POWER:def_2 ;
then (s1 . (n + 1)) / (s1 . n) <= (n / (n + 1)) #R 0 by A1, A14, A13, PREPOWER:84;
then (s1 . (n + 1)) / (s1 . n) <= 1 by A11, PREPOWER:71;
hence s1 . (n + 1) <= s1 . n by A12, XREAL_1:187; ::_thesis: verum
end;
end;
end;
hence s1 . (n + 1) <= s1 . n ; ::_thesis: verum
end;
then A15: s1 is V42() by SEQM_3:def_9;
A16: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_0_holds_
(s1_^\_1)_._n_>=_(s_^\_1)_._n
let n be Element of NAT ; ::_thesis: ( n >= 0 implies (s1 ^\ 1) . n >= (s ^\ 1) . n )
assume n >= 0 ; ::_thesis: (s1 ^\ 1) . n >= (s ^\ 1) . n
A17: 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, A17
.= s1 . (n + 1) by A6
.= (s1 ^\ 1) . n by NAT_1:def_3 ;
hence (s1 ^\ 1) . n >= (s ^\ 1) . n ; ::_thesis: verum
end;
deffunc H2( Element of NAT ) -> Element of REAL = $1 -root (s2 . $1);
consider s3 being Real_Sequence such that
A18: for n being Element of NAT holds s3 . n = H2(n) from SEQ_1:sch_1();
A19: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_s2_._n_=_2_to_power_((1_-_p)_*_n)_&_s2_._n_>=_0_&_s3_._n_=_n_-root_((2_to_power_(1_-_p))_to_power_n)_)
let n be Element of NAT ; ::_thesis: ( s2 . n = 2 to_power ((1 - p) * n) & s2 . n >= 0 & s3 . n = n -root ((2 to_power (1 - p)) to_power n) )
A20: 2 to_power n > 0 by POWER:34;
thus A21: s2 . n = (2 to_power n) * (s1 . (2 to_power n)) by A7
.= (2 to_power n) * (1 / ((2 to_power n) to_power p)) by A6, A20
.= (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) ; ::_thesis: ( s2 . n >= 0 & s3 . n = n -root ((2 to_power (1 - p)) to_power n) )
hence s2 . n >= 0 by POWER:34; ::_thesis: s3 . n = n -root ((2 to_power (1 - p)) to_power n)
s2 . n = (2 to_power (1 - p)) to_power n by A21, POWER:33;
hence s3 . n = n -root ((2 to_power (1 - p)) to_power n) by A18; ::_thesis: verum
end;
A22: now__::_thesis:_for_n_being_Nat_holds_(s3_^\_1)_._n_=_2_to_power_(1_-_p)
let n be Nat; ::_thesis: (s3 ^\ 1) . n = 2 to_power (1 - p)
A23: ( 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 A19
.= 2 to_power (1 - p) by A23, POWER:4 ; ::_thesis: verum
end;
then A24: s3 ^\ 1 is constant by VALUED_0:def_18;
then lim (s3 ^\ 1) = (s3 ^\ 1) . 0 by SEQ_4:26
.= 2 to_power (1 - p) by A22 ;
then A25: lim s3 = 2 to_power (1 - p) by A24, SEQ_4:22;
A26: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_s1_._n_>=_0_&_s2_._n_=_(2_to_power_n)_*_(s1_._(2_to_power_n))_)
let n be Element of NAT ; ::_thesis: ( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) )
now__::_thesis:_s1_._n_>=_0
percases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;
suppose n = 0 ; ::_thesis: s1 . n >= 0
hence s1 . n >= 0 by A6; ::_thesis: verum
end;
suppose ex m being Nat st n = m + 1 ; ::_thesis: s1 . n >= 0
then n to_power p > 0 by POWER:34;
then 1 / (n to_power p) >= 0 ;
hence s1 . n >= 0 by A6; ::_thesis: verum
end;
end;
end;
hence ( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) ) by A7; ::_thesis: verum
end;
A27: now__::_thesis:_for_n_being_Element_of_NAT_holds_(s_^\_1)_._n_>=_0
let n be Element of NAT ; ::_thesis: (s ^\ 1) . n >= 0
A28: n + 1 >= 0 + 1 by XREAL_1:6;
A29: s1 . (n + 1) >= 0 by A26;
(s ^\ 1) . n = s . (n + 1) by NAT_1:def_3
.= 1 / ((n + 1) to_power p) by A2, A28
.= s1 . (n + 1) by A6
.= (s1 ^\ 1) . n by NAT_1:def_3 ;
hence (s ^\ 1) . n >= 0 by A29, NAT_1:def_3; ::_thesis: verum
end;
A30: s3 is convergent by A24, SEQ_4:21;
1 - p < 0 by A1, XREAL_1:49;
then lim s3 < 1 by A25, POWER:36;
then s2 is summable by A18, A19, A30, Th28;
then s1 is summable by A15, A26, Th31;
then s1 ^\ 1 is summable by Th12;
then s ^\ 1 is summable by A27, A16, Th19;
hence s is summable by Th13; ::_thesis: verum
end;
theorem :: SERIES_1:33
for p being real number
for s being Real_Sequence st p <= 1 & ( for n being Element of NAT st n >= 1 holds
s . n = 1 / (n to_power p) ) holds
not s is summable
proof
let p be real number ; ::_thesis: for s being Real_Sequence st p <= 1 & ( for n being Element of NAT st n >= 1 holds
s . n = 1 / (n to_power p) ) holds
not s is summable
let s be Real_Sequence; ::_thesis: ( p <= 1 & ( for n being Element of NAT st n >= 1 holds
s . n = 1 / (n to_power p) ) implies not s is summable )
assume that
A1: p <= 1 and
A2: for n being Element of NAT st n >= 1 holds
s . n = 1 / (n to_power p) ; ::_thesis: not s is summable
now__::_thesis:_not_s_is_summable
percases ( p < 0 or p >= 0 ) ;
supposeA3: p < 0 ; ::_thesis: not s is summable
now__::_thesis:_(_s_is_convergent_implies_not_lim_s_=_0_)
assume ( s is convergent & lim s = 0 ) ; ::_thesis: contradiction
then consider m being Element of NAT such that
A4: for n being Element of NAT st n >= m holds
abs ((s . n) - 0) < 1 by SEQ_2:def_7;
consider k being Element of NAT such that
A5: k > m by SEQ_4:3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_not_n_>=_k
let n be Element of NAT ; ::_thesis: not n >= k
assume A6: n >= k ; ::_thesis: contradiction
A7: n > 0 by A5, A6;
then A8: n >= 0 + 1 by NAT_1:13;
n >= m by A5, A6, XXREAL_0:2;
then abs ((s . n) - 0) < 1 by A4;
then abs (1 / (n to_power p)) < 1 by A2, A8;
then abs (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; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
hence not s is summable by Th4; ::_thesis: verum
end;
supposeA10: p >= 0 ; ::_thesis: not s is summable
defpred S1[ Element of NAT , real number ] means ( ( $1 = 0 & $2 = 1 ) or ( $1 >= 1 & $2 = 1 / ($1 to_power p) ) );
A11: for n being Element of NAT ex r being Real st S1[n,r]
proof
let n be Element of NAT ; ::_thesis: ex r being Real st S1[n,r]
( n = 0 or n >= 1 )
proof
assume that
A12: n <> 0 and
A13: n < 1 ; ::_thesis: contradiction
n >= 0 + 1 by A12, NAT_1:13;
hence contradiction by A13; ::_thesis: verum
end;
hence ex r being Real st S1[n,r] ; ::_thesis: verum
end;
consider s1 being Real_Sequence such that
A14: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A11);
A15: s1 . 0 = 1 by A14;
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._(n_+_1)_<=_s1_._n
let n be Element of NAT ; ::_thesis: s1 . (n + 1) <= s1 . n
now__::_thesis:_s1_._(n_+_1)_<=_s1_._n
percases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;
supposeA16: n = 0 ; ::_thesis: s1 . (n + 1) <= s1 . n
then (n + 1) #R p >= 1 by A10, PREPOWER:85;
then A17: (n + 1) to_power p >= 1 by POWER:def_2;
s1 . (n + 1) = 1 / ((n + 1) to_power p) by A14;
hence s1 . (n + 1) <= s1 . n by A15, A16, A17, XREAL_1:211; ::_thesis: verum
end;
supposeA18: ex m being Nat st n = m + 1 ; ::_thesis: s1 . (n + 1) <= s1 . n
then n to_power p > 0 by POWER:34;
then 1 / (n to_power p) > 0 ;
then A19: s1 . n > 0 by A14;
A20: n / (n + 1) <= 1 by NAT_1:11, XREAL_1:183;
A21: n / (n + 1) > 0 by A18;
(s1 . (n + 1)) / (s1 . n) = (1 / ((n + 1) to_power p)) / (s1 . n) by A14
.= (1 / ((n + 1) to_power p)) / (1 / (n to_power p)) by A14, A18
.= (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 A18, POWER:31
.= (n / (n + 1)) #R p by A21, POWER:def_2 ;
then (s1 . (n + 1)) / (s1 . n) <= (n / (n + 1)) #R 0 by A10, A21, A20, PREPOWER:84;
then (s1 . (n + 1)) / (s1 . n) <= 1 by A18, PREPOWER:71;
hence s1 . (n + 1) <= s1 . n by A19, XREAL_1:187; ::_thesis: verum
end;
end;
end;
hence s1 . (n + 1) <= s1 . n ; ::_thesis: verum
end;
then A22: s1 is V42() by SEQM_3:def_9;
A23: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_1_holds_
s_._n_>=_s1_._n
let n be Element of NAT ; ::_thesis: ( n >= 1 implies s . n >= s1 . n )
assume A24: n >= 1 ; ::_thesis: s . n >= s1 . n
then s . n = 1 / (n to_power p) by A2
.= s1 . n by A14, A24 ;
hence s . n >= s1 . n ; ::_thesis: verum
end;
deffunc H1( Element of NAT ) -> Element of REAL = (2 to_power $1) * (s1 . (2 to_power $1));
consider s2 being Real_Sequence such that
A25: for n being Element of NAT holds s2 . n = H1(n) from SEQ_1:sch_1();
A26: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_s1_._n_>=_0_&_s2_._n_=_(2_to_power_n)_*_(s1_._(2_to_power_n))_)
let n be Element of NAT ; ::_thesis: ( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) )
now__::_thesis:_s1_._n_>=_0
percases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;
suppose n = 0 ; ::_thesis: s1 . n >= 0
hence s1 . n >= 0 by A14; ::_thesis: verum
end;
suppose ex m being Nat st n = m + 1 ; ::_thesis: s1 . n >= 0
then n to_power p > 0 by POWER:34;
then 1 / (n to_power p) >= 0 ;
hence s1 . n >= 0 by A14; ::_thesis: verum
end;
end;
end;
hence ( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) ) by A25; ::_thesis: verum
end;
now__::_thesis:_(_s2_is_convergent_implies_not_lim_s2_=_0_)
assume ( s2 is convergent & lim s2 = 0 ) ; ::_thesis: contradiction
then consider m being Element of NAT such that
A27: for n being Element of NAT st n >= m holds
abs ((s2 . n) - 0) < 1 / 2 by SEQ_2:def_7;
now__::_thesis:_for_n_being_Element_of_NAT_holds_not_n_>=_m
let n be Element of NAT ; ::_thesis: not n >= m
assume n >= m ; ::_thesis: contradiction
then abs ((s2 . n) - 0) < 1 / 2 by A27;
then A28: abs ((2 to_power n) * (s1 . (2 to_power n))) < 1 / 2 by A25;
2 to_power n >= 1 by PREPOWER:11;
then abs ((2 to_power n) * (1 / ((2 to_power n) to_power p))) < 1 / 2 by A14, A28;
then abs ((2 to_power n) * (1 / (2 to_power (n * p)))) < 1 / 2 by POWER:33;
then abs ((2 to_power n) * (2 to_power (- (n * p)))) < 1 / 2 by POWER:28;
then abs (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 by POWER:25;
then A29: 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 A29, POWER:def_2; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
then not s2 is summable by Th4;
then not s1 is summable by A22, A26, Th31;
hence not s is summable by A26, A23, Th19; ::_thesis: verum
end;
end;
end;
hence not s is summable ; ::_thesis: verum
end;
definition
let s be Real_Sequence;
attrs is absolutely_summable means :Def4: :: SERIES_1:def 4
abs s is summable ;
end;
:: deftheorem Def4 defines absolutely_summable SERIES_1:def_4_:_
for s being Real_Sequence holds
( s is absolutely_summable iff abs s is summable );
theorem Th34: :: SERIES_1:34
for s being Real_Sequence
for n, m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n))
proof
let s be Real_Sequence; ::_thesis: for n, m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n))
let n, m be Element of NAT ; ::_thesis: ( n <= m implies abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) )
assume A1: n <= m ; ::_thesis: abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n))
reconsider u = n, v = m as Integer ;
set s2 = Partial_Sums (abs s);
set s1 = Partial_Sums s;
defpred S1[ Element of NAT ] means abs (((Partial_Sums s) . (n + $1)) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . (n + $1)) - ((Partial_Sums (abs s)) . n));
now__::_thesis:_for_k_being_Element_of_NAT_holds_(abs_s)_._k_>=_0
let k be Element of NAT ; ::_thesis: (abs s) . k >= 0
abs (s . k) >= 0 by COMPLEX1:46;
hence (abs s) . k >= 0 by SEQ_1:12; ::_thesis: verum
end;
then A2: Partial_Sums (abs s) is V41() by Th16;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A4: abs (s . ((n + k) + 1)) >= 0 by COMPLEX1:46;
assume abs (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n)) ; ::_thesis: S1[k + 1]
then A5: (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))) <= (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n))) by XREAL_1:7;
A6: abs (((Partial_Sums (abs s)) . (n + (k + 1))) - ((Partial_Sums (abs s)) . n)) = abs ((((Partial_Sums (abs s)) . (n + k)) + ((abs s) . ((n + k) + 1))) - ((Partial_Sums (abs s)) . n)) by Def1
.= abs (((abs (s . ((n + k) + 1))) + ((Partial_Sums (abs s)) . (n + k))) - ((Partial_Sums (abs s)) . n)) by SEQ_1:12
.= abs ((abs (s . ((n + k) + 1))) + (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n))) ;
(Partial_Sums (abs s)) . (n + k) >= (Partial_Sums (abs s)) . n by A2, SEQM_3:5;
then A7: ((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n) >= 0 by XREAL_1:48;
abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) = abs (((s . ((n + k) + 1)) + ((Partial_Sums s) . (n + k))) - ((Partial_Sums s) . n)) by Def1
.= abs ((s . ((n + k) + 1)) + (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))) ;
then abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) <= (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))) by COMPLEX1:56;
then abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) <= (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n))) by A5, XXREAL_0:2;
then abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) <= (abs (s . ((n + k) + 1))) + (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n)) by A7, ABSVALUE:def_1;
hence S1[k + 1] by A7, A4, A6, ABSVALUE:def_1; ::_thesis: verum
end;
reconsider k = v - u as Element of NAT by A1, INT_1:5;
A8: n + k = m ;
A9: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A9, A3);
hence abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) by A8; ::_thesis: verum
end;
registration
cluster Function-like V18( NAT , REAL ) absolutely_summable -> summable for Element of K19(K20(NAT,REAL));
coherence
for b1 being Real_Sequence st b1 is absolutely_summable holds
b1 is summable
proof
let s be Real_Sequence; ::_thesis: ( s is absolutely_summable implies s is summable )
assume s is absolutely_summable ; ::_thesis: s is summable
then A1: abs s is summable by Def4;
now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_(((Partial_Sums_s)_._m)_-_((Partial_Sums_s)_._n))_<_r
let r be real number ; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r )
assume 0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) < r by A1, Th21;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r )
assume A3: n <= m ; ::_thesis: abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r
then A4: abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) by Th34;
abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) < r by A2, A3;
hence abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r by A4, XXREAL_0:2; ::_thesis: verum
end;
hence s is summable by Th21; ::_thesis: verum
end;
end;
theorem :: SERIES_1:35
for s being Real_Sequence st s is absolutely_summable holds
s is summable ;
theorem :: SERIES_1:36
for s being Real_Sequence st ( for n being Element of NAT holds 0 <= s . n ) & s is summable holds
s is absolutely_summable
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= s . n ) & s is summable implies s is absolutely_summable )
assume that
A1: for n being Element of NAT holds 0 <= s . n and
A2: s is summable ; ::_thesis: s is absolutely_summable
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_s_._n_=_abs_(s_._n)
let n be Element of NAT ; ::_thesis: s . n = abs (s . n)
0 <= s . n by A1;
hence s . n = abs (s . n) by ABSVALUE:def_1; ::_thesis: verum
end;
Partial_Sums s is convergent by A2, Def2;
then Partial_Sums (abs s) is convergent by A3, SEQ_1:12;
then abs s is summable by Def2;
hence s is absolutely_summable by Def4; ::_thesis: verum
end;
theorem :: SERIES_1:37
for s, s1 being Real_Sequence st ( for n being Element of NAT holds
( s . n <> 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) ) ) & s1 is convergent & lim s1 < 1 holds
s is absolutely_summable
proof
let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds
( s . n <> 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) ) ) & s1 is convergent & lim s1 < 1 implies s is absolutely_summable )
assume that
A1: for n being Element of NAT holds
( s . n <> 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) ) and
A2: ( s1 is convergent & lim s1 < 1 ) ; ::_thesis: s is absolutely_summable
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(abs_s)_._n_>_0_&_s1_._n_=_((abs_s)_._(n_+_1))_/_((abs_s)_._n)_)
let n be Element of NAT ; ::_thesis: ( (abs s) . n > 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) )
( (abs s) . n = abs (s . n) & s . n <> 0 ) by A1, SEQ_1:12;
hence (abs s) . n > 0 by COMPLEX1:47; ::_thesis: s1 . n = ((abs s) . (n + 1)) / ((abs s) . n)
thus s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) by A1; ::_thesis: verum
end;
then abs s is summable by A2, Th26;
hence s is absolutely_summable by Def4; ::_thesis: verum
end;
theorem Th38: :: SERIES_1:38
for r being real number
for s being Real_Sequence st r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs (s . n) >= r & s is convergent holds
lim s <> 0
proof
let r be real number ; ::_thesis: for s being Real_Sequence st r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs (s . n) >= r & s is convergent holds
lim s <> 0
let s be Real_Sequence; ::_thesis: ( r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs (s . n) >= r & s is convergent implies lim s <> 0 )
assume A1: r > 0 ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st
( n >= m & not abs (s . n) >= r ) or not s is convergent or lim s <> 0 )
given m being Element of NAT such that A2: for n being Element of NAT st n >= m holds
abs (s . n) >= r ; ::_thesis: ( not s is convergent or lim s <> 0 )
now__::_thesis:_(_not_s_is_convergent_or_lim_s_<>_0_)
percases ( not s is convergent or s is convergent ) ;
suppose not s is convergent ; ::_thesis: ( not s is convergent or lim s <> 0 )
hence ( not s is convergent or lim s <> 0 ) ; ::_thesis: verum
end;
supposeA3: s is convergent ; ::_thesis: ( not s is convergent or lim s <> 0 )
now__::_thesis:_not_lim_s_=_0
assume lim s = 0 ; ::_thesis: contradiction
then consider k being Element of NAT such that
A4: for n being Element of NAT st n >= k holds
abs ((s . n) - 0) < r by A1, A3, SEQ_2:def_7;
now__::_thesis:_for_n_being_Element_of_NAT_holds_not_n_>=_m_+_k
let n be Element of NAT ; ::_thesis: not n >= m + k
assume A5: n >= m + k ; ::_thesis: contradiction
m + k >= k by NAT_1:11;
then n >= k by A5, XXREAL_0:2;
then A6: abs ((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; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
hence ( not s is convergent or lim s <> 0 ) ; ::_thesis: verum
end;
end;
end;
hence ( not s is convergent or lim s <> 0 ) ; ::_thesis: verum
end;
theorem :: SERIES_1:39
for s being Real_Sequence st ( for n being Element of NAT holds s . n <> 0 ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
((abs s) . (n + 1)) / ((abs s) . n) >= 1 holds
not s is summable
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n <> 0 ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
((abs s) . (n + 1)) / ((abs s) . n) >= 1 implies not s is summable )
assume A1: for n being Element of NAT holds s . n <> 0 ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st
( n >= m & not ((abs s) . (n + 1)) / ((abs s) . n) >= 1 ) or not s is summable )
given m being Element of NAT such that A2: for n being Element of NAT st n >= m holds
((abs s) . (n + 1)) / ((abs s) . n) >= 1 ; ::_thesis: not s is summable
A3: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
abs_(s_._n)_>=_abs_(s_._m)
defpred S1[ Element of NAT ] means abs (s . (m + $1)) >= abs (s . m);
A4: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: abs (s . (m + k)) >= abs (s . m) ; ::_thesis: S1[k + 1]
((abs s) . ((m + k) + 1)) / ((abs s) . (m + k)) >= 1 by A2, NAT_1:11;
then (abs (s . ((m + k) + 1))) / ((abs s) . (m + k)) >= 1 by SEQ_1:12;
then A6: (abs (s . ((m + k) + 1))) / (abs (s . (m + k))) >= 1 by SEQ_1:12;
s . (m + k) <> 0 by A1;
then abs (s . (m + k)) > 0 by COMPLEX1:47;
then abs (s . ((m + k) + 1)) >= abs (s . (m + k)) by A6, XREAL_1:191;
hence S1[k + 1] by A5, XXREAL_0:2; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: ( n >= m implies abs (s . n) >= abs (s . m) )
assume n >= m ; ::_thesis: abs (s . n) >= abs (s . m)
then consider k being Nat such that
A7: n = m + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A8: n = m + k by A7;
A9: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A9, A4);
hence abs (s . n) >= abs (s . m) by A8; ::_thesis: verum
end;
s . m <> 0 by A1;
then abs (s . m) > 0 by COMPLEX1:47;
then ( not s is convergent or lim s <> 0 ) by A3, Th38;
hence not s is summable by Th4; ::_thesis: verum
end;
theorem :: SERIES_1:40
for s1, s being Real_Sequence st ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 < 1 holds
s is absolutely_summable
proof
let s1, s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 < 1 implies s is absolutely_summable )
assume that
A1: for n being Element of NAT holds s1 . n = n -root ((abs s) . n) and
A2: ( s1 is convergent & lim s1 < 1 ) ; ::_thesis: s is absolutely_summable
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(abs_s)_._n_>=_0_&_s1_._n_=_n_-root_((abs_s)_._n)_)
let n be Element of NAT ; ::_thesis: ( (abs s) . n >= 0 & s1 . n = n -root ((abs s) . n) )
(abs s) . n = abs (s . n) by SEQ_1:12;
hence (abs s) . n >= 0 by COMPLEX1:46; ::_thesis: s1 . n = n -root ((abs s) . n)
thus s1 . n = n -root ((abs s) . n) by A1; ::_thesis: verum
end;
then abs s is summable by A2, Th28;
hence s is absolutely_summable by Def4; ::_thesis: verum
end;
theorem :: SERIES_1:41
for s1, s being Real_Sequence st ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
s1 . n >= 1 holds
not s is summable
proof
let s1, s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
s1 . n >= 1 implies not s is summable )
assume A1: for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st
( m <= n & not s1 . n >= 1 ) or not s is summable )
given m being Element of NAT such that A2: for n being Element of NAT st m <= n holds
s1 . n >= 1 ; ::_thesis: not s is summable
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_+_1_holds_
abs_(s_._n)_>=_1
let n be Element of NAT ; ::_thesis: ( n >= m + 1 implies abs (s . n) >= 1 )
assume A3: n >= m + 1 ; ::_thesis: abs (s . n) >= 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 (abs (s . n)) by SEQ_1:12 ;
then ( abs (s . n) >= 0 & (n -root (abs (s . n))) |^ n >= 1 ) by A2, A5, COMPLEX1:46, PREPOWER:11;
hence abs (s . n) >= 1 by A4, POWER:4; ::_thesis: verum
end;
then ( not s is convergent or lim s <> 0 ) by Th38;
hence not s is summable by Th4; ::_thesis: verum
end;
theorem :: SERIES_1:42
for s1, s being Real_Sequence st ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 > 1 holds
not s is summable
proof
let s1, s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 > 1 implies not s is summable )
assume that
A1: for n being Element of NAT holds s1 . n = n -root ((abs s) . n) and
A2: s1 is convergent and
A3: lim s1 > 1 ; ::_thesis: not s is summable
(lim s1) - 1 > 0 by A3, XREAL_1:50;
then consider m being Element of NAT such that
A4: for n being Element of NAT st n >= m holds
abs ((s1 . n) - (lim s1)) < (lim s1) - 1 by A2, SEQ_2:def_7;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_+_1_holds_
abs_(s_._n)_>=_1
let n be Element of NAT ; ::_thesis: ( n >= m + 1 implies abs (s . n) >= 1 )
assume A5: n >= m + 1 ; ::_thesis: abs (s . n) >= 1
A6: s1 . n = n -root ((abs s) . n) by A1
.= n -root (abs (s . n)) by SEQ_1:12 ;
m + 1 >= m by NAT_1:11;
then n >= m by A5, XXREAL_0:2;
then abs ((n -root (abs (s . n))) - (lim s1)) < (lim s1) - 1 by A4, A6;
then - ((lim s1) - 1) < (n -root (abs (s . n))) - (lim s1) by SEQ_2:1;
then (1 - (lim s1)) + (lim s1) < ((n -root (abs (s . n))) - (lim s1)) + (lim s1) by XREAL_1:6;
then A7: ( abs (s . n) >= 0 & (n -root (abs (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 abs (s . n) >= 1 by A7, POWER:4; ::_thesis: verum
end;
then ( not s is convergent or lim s <> 0 ) by Th38;
hence not s is summable by Th4; ::_thesis: verum
end;
begin
definition
let s be Real_Sequence;
let n be Nat;
func Sum (s,n) -> Real equals :: SERIES_1:def 5
(Partial_Sums s) . n;
coherence
(Partial_Sums s) . n is Real ;
end;
:: deftheorem defines Sum SERIES_1:def_5_:_
for s being Real_Sequence
for n being Nat holds Sum (s,n) = (Partial_Sums s) . n;
definition
let s be Real_Sequence;
let n, m be Nat;
func Sum (s,n,m) -> Real equals :: SERIES_1:def 6
(Sum (s,n)) - (Sum (s,m));
coherence
(Sum (s,n)) - (Sum (s,m)) is Real ;
end;
:: deftheorem defines Sum SERIES_1:def_6_:_
for s being Real_Sequence
for n, m being Nat holds Sum (s,n,m) = (Sum (s,n)) - (Sum (s,m));