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

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

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

end;
let s1, s2 be sequence of X;

:: original: +

redefine func s1 + s2 -> sequence of X;

coherence

s1 + s2 is sequence of X

proof end;

definition

let s be complex-valued ManySortedSet of NAT ;

ex b_{1} being complex-valued ManySortedSet of NAT st

( b_{1} . 0 = s . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) + (s . (n + 1)) ) )

for b_{1}, b_{2} being complex-valued ManySortedSet of NAT st b_{1} . 0 = s . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) + (s . (n + 1)) ) & b_{2} . 0 = s . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) + (s . (n + 1)) ) holds

b_{1} = b_{2}

end;
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 ( it . 0 = s . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (s . (n + 1)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Partial_Sums SERIES_1:def 1 :

for s, b_{2} being complex-valued ManySortedSet of NAT holds

( b_{2} = Partial_Sums s iff ( b_{2} . 0 = s . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) + (s . (n + 1)) ) ) );

for s, b

( b

registration
end;

definition

let s be Real_Sequence;

:: original: Partial_Sums

redefine func Partial_Sums s -> Real_Sequence;

coherence

Partial_Sums s is Real_Sequence

end;
:: original: Partial_Sums

redefine func Partial_Sums s -> Real_Sequence;

coherence

Partial_Sums s is Real_Sequence

proof end;

:: deftheorem Def2 defines summable SERIES_1:def 2 :

for s being Real_Sequence holds

( s is summable iff Partial_Sums s is convergent );

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

for s being Real_Sequence holds Sum s = lim (Partial_Sums s);

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)

for s1, s2 being sequence of X 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) )

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

( s1 - s2 is summable & Sum (s1 - s2) = (Sum s1) - (Sum s2) )

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

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

Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1

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

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

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

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 )

( Partial_Sums s is bounded_above iff s is summable )

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

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 )

( 0 <= s1 . n & s1 . n <= s2 . n ) ) & s2 is summable holds

( s1 is summable & Sum s1 <= Sum s2 )

proof end;

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

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)

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

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

( 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

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

( 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

( 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

( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 > 1 holds

not s is summable

proof end;

registration
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;
:: 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;

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 )

( 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

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;

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

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

:: deftheorem defines absolutely_summable SERIES_1:def 4 :

for s being Real_Sequence holds

( s is absolutely_summable iff abs s is summable );

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

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

for b_{1} being Real_Sequence st b_{1} is absolutely_summable holds

b_{1} is summable
end;

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

coherence for b

b

proof end;

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

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

( 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

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

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

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

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

not s is summable

proof end;

:: from BHSP_4, 2006.03.04, A.T.

:: deftheorem defines Sum SERIES_1:def 5 :

for s being Real_Sequence

for n being Nat holds Sum (s,n) = (Partial_Sums s) . n;

for s being Real_Sequence

for n being Nat holds Sum (s,n) = (Partial_Sums s) . n;

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

for s being Real_Sequence

for n, m being Nat holds Sum (s,n,m) = (Sum (s,n)) - (Sum (s,m));