:: Series
:: by Konrad Raczkowski and Andrzej N\c{e}dzusiak
::
:: Received October 15, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th1: :: SERIES_1:1

for a being Real
for s being Real_Sequence st 0 < a & a < 1 & ( for n being Nat holds s . n = a to_power (n + 1) ) holds
( s is convergent & lim s = 0 )

proof end;

theorem Th2: :: SERIES_1:2

for a being Real
for n being Nat holds |.a.| to_power n = |.(a to_power n).|

proof end;

theorem Th3: :: SERIES_1:3

for a being Real
for s being Real_Sequence st |.a.| < 1 & ( for n being Nat holds s . n = a to_power (n + 1) ) holds
( s is convergent & lim s = 0 )

proof end;

definition

let X be non empty complex-membered add-closed set ;
let s1, s2 be sequence of X;
:: original: +
redefine func s1 + s2 -> sequence of X;
coherence
s1 + s2 is sequence of X

proof 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 Nat holds it . (n + 1) = (it . n) + (s . (n + 1)) ) );

existence
ex b₁ being complex-valued ManySortedSet of NAT st
( b₁ . 0 = s . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) + (s . (n + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being complex-valued ManySortedSet of NAT st b₁ . 0 = s . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) + (s . (n + 1)) ) & b₂ . 0 = s . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) + (s . (n + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Partial_Sums SERIES_1:def 1 :
for s, b₂ being complex-valued ManySortedSet of NAT holds
( b₂ = Partial_Sums s iff ( b₂ . 0 = s . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . 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 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 end;

end;

definition

let s be Real_Sequence;

attr s 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 end;

Lm1: for seq, seq1, seq2 being complex-valued ManySortedSet of NAT holds
( seq = seq1 + seq2 iff for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) )

proof 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 end;

theorem Th6: :: SERIES_1:6

for s1, s2 being Real_Sequence holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)

proof 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 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 end;

theorem Th9: :: SERIES_1:9

for r being Real
for s being Real_Sequence holds Partial_Sums (r (#) s) = r (#) (Partial_Sums s)

proof end;

theorem Th10: :: SERIES_1:10

for r being Real
for s being Real_Sequence st s is summable holds
( r (#) s is summable & Sum (r (#) s) = r * (Sum s) )

proof end;

theorem Th11: :: SERIES_1:11

for s, s1 being Real_Sequence st ( for n being Nat holds s1 . n = s . 0 ) holds
Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1

proof end;

theorem Th12: :: SERIES_1:12

for s being Real_Sequence st s is summable holds
for n being Nat holds s ^\ n is summable

proof end;

theorem Th13: :: SERIES_1:13

for s being Real_Sequence st ex n being Nat st s ^\ n is summable holds
s is summable

proof end;

theorem Th14: :: SERIES_1:14

for s1, s2 being Real_Sequence st ( for n being Nat holds s1 . n <= s2 . n ) holds
for n being Nat holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n

proof end;

theorem :: SERIES_1:15

for s being Real_Sequence st s is summable holds
for n being Nat holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1)))

proof end;

theorem Th16: :: SERIES_1:16

for s being Real_Sequence st ( for n being Nat holds 0 <= s . n ) holds
Partial_Sums s is V47()

proof end;

theorem Th17: :: SERIES_1:17

for s being Real_Sequence st ( for n being Nat holds 0 <= s . n ) holds
( Partial_Sums s is bounded_above iff s is summable )

proof end;

theorem :: SERIES_1:18

for s being Real_Sequence st s is summable & ( for n being Nat holds 0 <= s . n ) holds
0 <= Sum s

proof end;

theorem Th19: :: SERIES_1:19

for s1, s2 being Real_Sequence st ( for n being Nat holds 0 <= s2 . n ) & s1 is summable & ex m being Nat st
for n being Nat st m <= n holds
s2 . n <= s1 . n holds
s2 is summable

proof end;

theorem :: SERIES_1:20

for s1, s2 being Real_Sequence st ( for n being Nat holds
( 0 <= s1 . n & s1 . n <= s2 . n ) ) & s2 is summable holds
( s1 is summable & Sum s1 <= Sum s2 )

proof end;

theorem Th21: :: SERIES_1:21

for s being Real_Sequence holds
( s is summable iff for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r ) by SEQ_4:41;

:: Sum of a Geometric Series

theorem Th22: :: SERIES_1:22

for n being Nat
for a being Real st a <> 1 holds
(Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a)

proof end;

theorem :: SERIES_1:23

for a being Real
for s being Real_Sequence st a <> 1 & ( for n being Nat holds s . (n + 1) = a * (s . n) ) holds
for n being Nat holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a)

proof end;

theorem Th24: :: SERIES_1:24

for a being Real st |.a.| < 1 holds
( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) )

proof end;

theorem :: SERIES_1:25

for a being Real
for s being Real_Sequence st |.a.| < 1 & ( for n being Nat holds s . (n + 1) = a * (s . n) ) holds
( s is summable & Sum s = (s . 0) / (1 - a) )

proof end;

theorem Th26: :: SERIES_1:26

for s, s1 being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s1 . n = (s . (n + 1)) / (s . n) ) ) & s1 is convergent & lim s1 < 1 holds
s is summable

proof end;

theorem :: SERIES_1:27

for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) & ex m being Nat st
for n being Nat st n >= m holds
(s . (n + 1)) / (s . n) >= 1 holds
not s is summable

proof end;

theorem Th28: :: SERIES_1:28

for s, s1 being Real_Sequence st ( for n being Nat holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 < 1 holds
s is summable

proof end;

theorem Th29: :: SERIES_1:29

for s, s1 being Real_Sequence st ( for n being Nat holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & ex m being Nat st
for n being Nat st m <= n holds
s1 . n >= 1 holds
not s is summable

proof end;

theorem :: SERIES_1:30

for s, s1 being Real_Sequence st ( for n being Nat holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 > 1 holds
not s is summable

proof end;

registration

let k, n be Nat;

cluster k to_power n -> natural ;

coherence
k to_power n is natural ;

end;

definition

let k, n be Nat;
:: original: to_power
redefine func k 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 V48() & ( for n being 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 end;

Lm2: 1 in REAL
by XREAL_0:def 1;

theorem :: SERIES_1:32

for p being Real
for s being Real_Sequence st p > 1 & ( for n being Nat st n >= 1 holds
s . n = 1 / (n to_power p) ) holds
s is summable

proof end;

:: Divergence of the Harmonic Series

theorem :: SERIES_1:33

for p being Real
for s being Real_Sequence st p <= 1 & ( for n being Nat st n >= 1 holds
s . n = 1 / (n to_power p) ) holds
not s is summable

proof end;

definition

let s be Real_Sequence;

attr s is absolutely_summable means :: SERIES_1:def 4
abs s is summable ;

end;

:: deftheorem 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 Nat st n <= m holds
|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| <= |.(((Partial_Sums |.s.|) . m) - ((Partial_Sums |.s.|) . n)).|

proof end;

registration

cluster Function-like V18( omega , REAL ) absolutely_summable -> summable for Element of K19(K20(omega,REAL));

coherence
for b₁ being Real_Sequence st b₁ is absolutely_summable holds
b₁ is summable

proof 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 Nat holds 0 <= s . n ) & s is summable holds
s is absolutely_summable

proof end;

theorem :: SERIES_1:37

for s, s1 being Real_Sequence st ( for n being 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 end;

theorem Th38: :: SERIES_1:38

for r being Real
for s being Real_Sequence st r > 0 & ex m being Nat st
for n being Nat st n >= m holds
|.(s . n).| >= r & s is convergent holds
lim s <> 0

proof end;

theorem :: SERIES_1:39

for s being Real_Sequence st ( for n being Nat holds s . n <> 0 ) & ex m being Nat st
for n being Nat st n >= m holds
((abs s) . (n + 1)) / ((abs s) . n) >= 1 holds
not s is summable

proof end;

theorem :: SERIES_1:40

for s, s1 being Real_Sequence st ( for n being Nat holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 < 1 holds
s is absolutely_summable

proof end;

theorem :: SERIES_1:41

for s, s1 being Real_Sequence st ( for n being Nat holds s1 . n = n -root ((abs s) . n) ) & ex m being Nat st
for n being Nat st m <= n holds
s1 . n >= 1 holds
not s is summable

proof end;

theorem :: SERIES_1:42

for s, s1 being Real_Sequence st ( for n being Nat holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 > 1 holds
not s is summable

proof end;

:: from BHSP_4, 2006.03.04, A.T.

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));