:: Series in Banach and Hilbert Spaces
:: by El\.zbieta Kraszewska and Jan Popio{\l}ek
::
:: Received April 1, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

deffunc H1( RealUnitarySpace) -> Element of the carrier of $1 = 0. $1;

definition
let X be non empty addLoopStr ;
let seq be sequence of X;
func Partial_Sums seq -> sequence of X means :Def1: :: BHSP_4:def 1
( it . 0 = seq . 0 & ( for n being Element of NAT holds it . (n + 1) = (it . n) + (seq . (n + 1)) ) );
existence
ex b1 being sequence of X st
( b1 . 0 = seq . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (seq . (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being sequence of X st b1 . 0 = seq . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (seq . (n + 1)) ) & b2 . 0 = seq . 0 & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) + (seq . (n + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Partial_Sums BHSP_4:def 1 :
for X being non empty addLoopStr
for seq, b3 being sequence of X holds
( b3 = Partial_Sums seq iff ( b3 . 0 = seq . 0 & ( for n being Element of NAT holds b3 . (n + 1) = (b3 . n) + (seq . (n + 1)) ) ) );

theorem Th1: :: BHSP_4:1
for X being non empty Abelian add-associative addLoopStr
for seq1, seq2 being sequence of X holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2)
proof end;

theorem Th2: :: BHSP_4:2
for X being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for seq1, seq2 being sequence of X holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2)
proof end;

theorem Th3: :: BHSP_4:3
for a being Real
for X being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for seq being sequence of X holds Partial_Sums (a * seq) = a * (Partial_Sums seq)
proof end;

theorem :: BHSP_4:4
for X being RealUnitarySpace
for seq being sequence of X holds Partial_Sums (- seq) = - (Partial_Sums seq)
proof end;

theorem :: BHSP_4:5
for a, b being Real
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds (a * (Partial_Sums seq1)) + (b * (Partial_Sums seq2)) = Partial_Sums ((a * seq1) + (b * seq2))
proof end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
attr seq is summable means :Def2: :: BHSP_4:def 2
 Partial_Sums seq is convergent ;
func Sum seq -> Point of X equals :: BHSP_4:def 3
 lim (Partial_Sums seq);
coherence
lim (Partial_Sums seq) is Point of X ;
end;

:: deftheorem Def2 defines summable BHSP_4:def 2 :
for X being RealUnitarySpace
for seq being sequence of X holds
( seq is summable iff Partial_Sums seq is convergent );

:: deftheorem defines Sum BHSP_4:def 3 :
for X being RealUnitarySpace
for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);

theorem :: BHSP_4:6
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
proof end;

theorem :: BHSP_4:7
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
proof end;

theorem :: BHSP_4:8
for a being Real
for X being RealUnitarySpace
for seq being sequence of X st seq is summable holds
( a * seq is summable & Sum (a * seq) = a * (Sum seq) )
proof end;

theorem Th9: :: BHSP_4:9
for X being RealUnitarySpace
for seq being sequence of X st seq is summable holds
( seq is convergent & lim seq = 0. X )
proof end;

theorem Th10: :: BHSP_4:10
for X being RealHilbertSpace
for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r )
proof end;

theorem :: BHSP_4:11
for X being RealUnitarySpace
for seq being sequence of X st seq is summable holds
Partial_Sums seq is bounded
proof end;

theorem Th12: :: BHSP_4:12
for X being RealUnitarySpace
for seq, seq1 being sequence of X st ( for n being Element of NAT holds seq1 . n = seq . 0 ) holds
Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
proof end;

theorem Th13: :: BHSP_4:13
for X being RealUnitarySpace
for seq being sequence of X st seq is summable holds
for k being Element of NAT holds seq ^\ k is summable
proof end;

theorem :: BHSP_4:14
for X being RealUnitarySpace
for seq being sequence of X st ex k being Element of NAT st seq ^\ k is summable holds
seq is summable
proof end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
let n be Element of NAT ;
func Sum (seq,n) -> Point of X equals :: BHSP_4:def 4
(Partial_Sums seq) . n;
coherence
(Partial_Sums seq) . n is Point of X ;
end;

:: deftheorem defines Sum BHSP_4:def 4 :
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds Sum (seq,n) = (Partial_Sums seq) . n;

theorem :: BHSP_4:15
for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,0) = seq . 0 by Def1;

theorem Th16: :: BHSP_4:16
for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,1) = (Sum (seq,0)) + (seq . 1)
proof end;

theorem Th17: :: BHSP_4:17
for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,1) = (seq . 0) + (seq . 1)
proof end;

theorem :: BHSP_4:18
for n being Element of NAT
for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,(n + 1)) = (Sum (seq,n)) + (seq . (n + 1)) by Def1;

theorem Th19: :: BHSP_4:19
for n being Element of NAT
for X being RealUnitarySpace
for seq being sequence of X holds seq . (n + 1) = (Sum (seq,(n + 1))) - (Sum (seq,n))
proof end;

theorem :: BHSP_4:20
for X being RealUnitarySpace
for seq being sequence of X holds seq . 1 = (Sum (seq,1)) - (Sum (seq,0))
proof end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
let n, m be Element of NAT ;
func Sum (seq,n,m) -> Point of X equals :: BHSP_4:def 5
(Sum (seq,n)) - (Sum (seq,m));
coherence
(Sum (seq,n)) - (Sum (seq,m)) is Point of X ;
end;

:: deftheorem defines Sum BHSP_4:def 5 :
for X being RealUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds Sum (seq,n,m) = (Sum (seq,n)) - (Sum (seq,m));

theorem :: BHSP_4:21
for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,1,0) = seq . 1
proof end;

theorem :: BHSP_4:22
for n being Element of NAT
for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,(n + 1),n) = seq . (n + 1) by Th19;

theorem Th23: :: BHSP_4:23
for X being RealHilbertSpace
for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )
proof end;

theorem :: BHSP_4:24
for X being RealHilbertSpace
for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.(Sum (seq,n,m)).|| < r )
proof end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
attr seq is absolutely_summable means :Def6: :: BHSP_4:def 6
||.seq.|| is summable ;
end;

:: deftheorem Def6 defines absolutely_summable BHSP_4:def 6 :
for X being RealUnitarySpace
for seq being sequence of X holds
( seq is absolutely_summable iff ||.seq.|| is summable );

theorem :: BHSP_4:25
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is absolutely_summable & seq2 is absolutely_summable holds
seq1 + seq2 is absolutely_summable
proof end;

theorem :: BHSP_4:26
for a being Real
for X being RealUnitarySpace
for seq being sequence of X st seq is absolutely_summable holds
a * seq is absolutely_summable
proof end;

theorem :: BHSP_4:27
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds
seq is absolutely_summable
proof end;

theorem :: BHSP_4:28
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds
( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
proof end;

theorem Th29: :: BHSP_4:29
for r being Real
for X being RealUnitarySpace
for seq being sequence of X st r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . n).|| >= r & seq is convergent holds
lim seq <> 0. X
proof end;

theorem Th30: :: BHSP_4:30
for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 holds
not seq is summable
proof end;

theorem :: BHSP_4:31
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) & ( for n being Element of NAT holds Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
proof end;

theorem :: BHSP_4:32
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
proof end;

theorem :: BHSP_4:33
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
Rseq . n >= 1 holds
not seq is summable
proof end;

theorem :: BHSP_4:34
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
proof end;

theorem Th35: :: BHSP_4:35
for X being RealUnitarySpace
for seq being sequence of X holds Partial_Sums ||.seq.|| is non-decreasing
proof end;

theorem :: BHSP_4:36
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ||.seq.||) . n >= 0
proof end;

theorem Th37: :: BHSP_4:37
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n
proof end;

theorem :: BHSP_4:38
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n) by Th37;

theorem Th39: :: BHSP_4:39
for X being RealUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))
proof end;

theorem :: BHSP_4:40
for X being RealUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds ||.((Sum (seq,m)) - (Sum (seq,n))).|| <= abs ((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))) by Th39;

theorem :: BHSP_4:41
for X being RealUnitarySpace
for seq being sequence of X
for n, m being Element of NAT holds ||.(Sum (seq,m,n)).|| <= abs (Sum (||.seq.||,m,n)) by Th39;

theorem :: BHSP_4:42
for X being RealHilbertSpace
for seq being sequence of X st seq is absolutely_summable holds
seq is summable
proof end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
let Rseq be Real_Sequence;
func Rseq * seq -> sequence of X means :Def7: :: BHSP_4:def 7
 for n being Element of NAT holds it . n = (Rseq . n) * (seq . n);
existence
ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (Rseq . n) * (seq . n)
proof end;
uniqueness
for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (Rseq . n) * (seq . n) ) & ( for n being Element of NAT holds b2 . n = (Rseq . n) * (seq . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines * BHSP_4:def 7 :
for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence
for b4 being sequence of X holds
( b4 = Rseq * seq iff for n being Element of NAT holds b4 . n = (Rseq . n) * (seq . n) );

theorem :: BHSP_4:43
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds Rseq * (seq1 + seq2) = (Rseq * seq1) + (Rseq * seq2)
proof end;

theorem :: BHSP_4:44
for Rseq1, Rseq2 being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds (Rseq1 + Rseq2) * seq = (Rseq1 * seq) + (Rseq2 * seq)
proof end;

theorem :: BHSP_4:45
for Rseq1, Rseq2 being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq)
proof end;

theorem Th46: :: BHSP_4:46
for a being Real
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds (a (#) Rseq) * seq = a * (Rseq * seq)
proof end;

theorem :: BHSP_4:47
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds Rseq * (- seq) = (- Rseq) * seq
proof end;

theorem Th48: :: BHSP_4:48
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st Rseq is convergent & seq is convergent holds
Rseq * seq is convergent
proof end;

theorem :: BHSP_4:49
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st Rseq is bounded & seq is bounded holds
Rseq * seq is bounded
proof end;

theorem :: BHSP_4:50
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st Rseq is convergent & seq is convergent holds
( Rseq * seq is convergent & lim (Rseq * seq) = (lim Rseq) * (lim seq) )
proof end;

definition
let Rseq be Real_Sequence;
attr Rseq is Cauchy means :Def8: :: BHSP_4:def 8
 for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
abs ((Rseq . n) - (Rseq . m)) < r;
end;

:: deftheorem Def8 defines Cauchy BHSP_4:def 8 :
for Rseq being Real_Sequence holds
( Rseq is Cauchy iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
abs ((Rseq . n) - (Rseq . m)) < r );

theorem :: BHSP_4:51
for Rseq being Real_Sequence
for X being RealHilbertSpace
for seq being sequence of X st seq is Cauchy & Rseq is Cauchy holds
Rseq * seq is Cauchy
proof end;

theorem Th52: :: BHSP_4:52
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))
proof end;

theorem Th53: :: BHSP_4:53
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds (Partial_Sums (Rseq * seq)) . (n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Partial_Sums (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq))) . n)
proof end;

theorem :: BHSP_4:54
for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds Sum ((Rseq * seq),(n + 1)) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - (Sum ((((Rseq ^\ 1) - Rseq) * (Partial_Sums seq)),n)) by Th53;