:: BHSP_4 semantic presentation

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

scheme :: BHSP_4:sch 1
s1{ F1() -> RealUnitarySpace, F2() -> Point of F1(), F3( Nat, Point of F1()) -> Point of F1() } :
ex b1 being Function of NAT ,the carrier of F1() st
( b1 . 0 = F2() & ( for b2 being Element of NAT
for b3 being Point of F1() st b3 = b1 . b2 holds
b1 . (b2 + 1) = F3(b2,b3) ) )
proof end;

definition
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
func Partial_Sums c2 -> sequence of a1 means :Def1: :: BHSP_4:def 1
( a3 . 0 = a2 . 0 & ( for b1 being Nat holds a3 . (b1 + 1) = (a3 . b1) + (a2 . (b1 + 1)) ) );
existence
ex b1 being sequence of c1 st
( b1 . 0 = c2 . 0 & ( for b2 being Nat holds b1 . (b2 + 1) = (b1 . b2) + (c2 . (b2 + 1)) ) )
proof end;
uniqueness
for b1, b2 being sequence of c1 st b1 . 0 = c2 . 0 & ( for b3 being Nat holds b1 . (b3 + 1) = (b1 . b3) + (c2 . (b3 + 1)) ) & b2 . 0 = c2 . 0 & ( for b3 being Nat holds b2 . (b3 + 1) = (b2 . b3) + (c2 . (b3 + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Partial_Sums BHSP_4:def 1 :
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 holds
( b3 = Partial_Sums b2 iff ( b3 . 0 = b2 . 0 & ( for b4 being Nat holds b3 . (b4 + 1) = (b3 . b4) + (b2 . (b4 + 1)) ) ) );

theorem Th1: :: BHSP_4:1
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 holds (Partial_Sums b2) + (Partial_Sums b3) = Partial_Sums (b2 + b3)
proof end;

theorem Th2: :: BHSP_4:2
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 holds (Partial_Sums b2) - (Partial_Sums b3) = Partial_Sums (b2 - b3)
proof end;

theorem Th3: :: BHSP_4:3
for b1 being RealUnitarySpace
for b2 being Real
for b3 being sequence of b1 holds Partial_Sums (b2 * b3) = b2 * (Partial_Sums b3)
proof end;

theorem Th4: :: BHSP_4:4
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds Partial_Sums (- b2) = - (Partial_Sums b2)
proof end;

theorem Th5: :: BHSP_4:5
for b1 being RealUnitarySpace
for b2, b3 being Real
for b4, b5 being sequence of b1 holds (b2 * (Partial_Sums b4)) + (b3 * (Partial_Sums b5)) = Partial_Sums ((b2 * b4) + (b3 * b5))
proof end;

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

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

:: deftheorem Def3 defines Sum BHSP_4:def 3 :
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds Sum b2 = lim (Partial_Sums b2);

theorem Th6: :: BHSP_4:6
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 st b2 is summable & b3 is summable holds
( b2 + b3 is summable & Sum (b2 + b3) = (Sum b2) + (Sum b3) )
proof end;

theorem Th7: :: BHSP_4:7
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 st b2 is summable & b3 is summable holds
( b2 - b3 is summable & Sum (b2 - b3) = (Sum b2) - (Sum b3) )
proof end;

theorem Th8: :: BHSP_4:8
for b1 being RealUnitarySpace
for b2 being Real
for b3 being sequence of b1 st b3 is summable holds
( b2 * b3 is summable & Sum (b2 * b3) = b2 * (Sum b3) )
proof end;

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

theorem Th10: :: BHSP_4:10
for b1 being RealUnitarySpace
for b2 being sequence of b1 st b1 is_Hilbert_space holds
( b2 is summable iff for b3 being Real st b3 > 0 holds
ex b4 being Nat st
for b5, b6 being Nat st b5 >= b4 & b6 >= b4 holds
||.(((Partial_Sums b2) . b5) - ((Partial_Sums b2) . b6)).|| < b3 )
proof end;

theorem Th11: :: BHSP_4:11
for b1 being RealUnitarySpace
for b2 being sequence of b1 st b2 is summable holds
Partial_Sums b2 is bounded
proof end;

theorem Th12: :: BHSP_4:12
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 st ( for b4 being Nat holds b3 . b4 = b2 . 0 ) holds
Partial_Sums (b2 ^\ 1) = ((Partial_Sums b2) ^\ 1) - b3
proof end;

theorem Th13: :: BHSP_4:13
for b1 being RealUnitarySpace
for b2 being sequence of b1 st b2 is summable holds
for b3 being Nat holds b2 ^\ b3 is summable
proof end;

theorem Th14: :: BHSP_4:14
for b1 being RealUnitarySpace
for b2 being sequence of b1 st ex b3 being Nat st b2 ^\ b3 is summable holds
b2 is summable
proof end;

definition
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
let c3 be Nat;
func Sum c2,c3 -> Point of a1 equals :: BHSP_4:def 4
(Partial_Sums a2) . a3;
coherence
(Partial_Sums c2) . c3 is Point of c1
;
end;

:: deftheorem Def4 defines Sum BHSP_4:def 4 :
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Nat holds Sum b2,b3 = (Partial_Sums b2) . b3;

theorem Th15: :: BHSP_4:15
canceled;

theorem Th16: :: BHSP_4:16
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds Sum b2,0 = b2 . 0 by Def1;

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

theorem Th18: :: BHSP_4:18
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds Sum b2,1 = (b2 . 0) + (b2 . 1)
proof end;

theorem Th19: :: BHSP_4:19
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Nat holds Sum b2,(b3 + 1) = (Sum b2,b3) + (b2 . (b3 + 1)) by Def1;

theorem Th20: :: BHSP_4:20
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Nat holds b2 . (b3 + 1) = (Sum b2,(b3 + 1)) - (Sum b2,b3)
proof end;

theorem Th21: :: BHSP_4:21
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds b2 . 1 = (Sum b2,1) - (Sum b2,0)
proof end;

definition
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
let c3, c4 be Nat;
func Sum c2,c3,c4 -> Point of a1 equals :: BHSP_4:def 5
(Sum a2,a3) - (Sum a2,a4);
coherence
(Sum c2,c3) - (Sum c2,c4) is Point of c1
;
end;

:: deftheorem Def5 defines Sum BHSP_4:def 5 :
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3, b4 being Nat holds Sum b2,b3,b4 = (Sum b2,b3) - (Sum b2,b4);

theorem Th22: :: BHSP_4:22
canceled;

theorem Th23: :: BHSP_4:23
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds Sum b2,1,0 = b2 . 1
proof end;

theorem Th24: :: BHSP_4:24
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Nat holds Sum b2,(b3 + 1),b3 = b2 . (b3 + 1) by Th20;

theorem Th25: :: BHSP_4:25
for b1 being RealUnitarySpace
for b2 being sequence of b1 st b1 is_Hilbert_space holds
( b2 is summable iff for b3 being Real st b3 > 0 holds
ex b4 being Nat st
for b5, b6 being Nat st b5 >= b4 & b6 >= b4 holds
||.((Sum b2,b5) - (Sum b2,b6)).|| < b3 )
proof end;

theorem Th26: :: BHSP_4:26
for b1 being RealUnitarySpace
for b2 being sequence of b1 st b1 is_Hilbert_space holds
( b2 is summable iff for b3 being Real st b3 > 0 holds
ex b4 being Nat st
for b5, b6 being Nat st b5 >= b4 & b6 >= b4 holds
||.(Sum b2,b5,b6).|| < b3 )
proof end;

definition
let c1 be Real_Sequence;
let c2 be Nat;
func Sum c1,c2 -> Real equals :: BHSP_4:def 6
(Partial_Sums a1) . a2;
coherence
(Partial_Sums c1) . c2 is Real
;
end;

:: deftheorem Def6 defines Sum BHSP_4:def 6 :
for b1 being Real_Sequence
for b2 being Nat holds Sum b1,b2 = (Partial_Sums b1) . b2;

definition
let c1 be Real_Sequence;
let c2, c3 be Nat;
func Sum c1,c2,c3 -> Real equals :: BHSP_4:def 7
(Sum a1,a2) - (Sum a1,a3);
coherence
(Sum c1,c2) - (Sum c1,c3) is Real
;
end;

:: deftheorem Def7 defines Sum BHSP_4:def 7 :
for b1 being Real_Sequence
for b2, b3 being Nat holds Sum b1,b2,b3 = (Sum b1,b2) - (Sum b1,b3);

definition
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
attr a2 is absolutely_summable means :Def8: :: BHSP_4:def 8
||.a2.|| is summable;
end;

:: deftheorem Def8 defines absolutely_summable BHSP_4:def 8 :
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds
( b2 is absolutely_summable iff ||.b2.|| is summable );

theorem Th27: :: BHSP_4:27
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 st b2 is absolutely_summable & b3 is absolutely_summable holds
b2 + b3 is absolutely_summable
proof end;

theorem Th28: :: BHSP_4:28
for b1 being RealUnitarySpace
for b2 being Real
for b3 being sequence of b1 st b3 is absolutely_summable holds
b2 * b3 is absolutely_summable
proof end;

theorem Th29: :: BHSP_4:29
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence st ( for b4 being Nat holds ||.b2.|| . b4 <= b3 . b4 ) & b3 is summable holds
b2 is absolutely_summable
proof end;

theorem Th30: :: BHSP_4:30
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence st ( for b4 being Nat holds
( b2 . b4 <> 0. b1 & b3 . b4 = ||.(b2 . (b4 + 1)).|| / ||.(b2 . b4).|| ) ) & b3 is convergent & lim b3 < 1 holds
b2 is absolutely_summable
proof end;

theorem Th31: :: BHSP_4:31
for b1 being RealUnitarySpace
for b2 being Real
for b3 being sequence of b1 st b2 > 0 & ex b4 being Nat st
for b5 being Nat st b5 >= b4 holds
||.(b3 . b5).|| >= b2 & b3 is convergent holds
lim b3 <> 0. b1
proof end;

theorem Th32: :: BHSP_4:32
for b1 being RealUnitarySpace
for b2 being sequence of b1 st ( for b3 being Nat holds b2 . b3 <> 0. b1 ) & ex b3 being Nat st
for b4 being Nat st b4 >= b3 holds
||.(b2 . (b4 + 1)).|| / ||.(b2 . b4).|| >= 1 holds
not b2 is summable
proof end;

theorem Th33: :: BHSP_4:33
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence st ( for b4 being Nat holds b2 . b4 <> 0. b1 ) & ( for b4 being Nat holds b3 . b4 = ||.(b2 . (b4 + 1)).|| / ||.(b2 . b4).|| ) & b3 is convergent & lim b3 > 1 holds
not b2 is summable
proof end;

theorem Th34: :: BHSP_4:34
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence st ( for b4 being Nat holds b3 . b4 = b4 -root ||.(b2 . b4).|| ) & b3 is convergent & lim b3 < 1 holds
b2 is absolutely_summable
proof end;

theorem Th35: :: BHSP_4:35
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence st ( for b4 being Nat holds b3 . b4 = b4 -root (||.b2.|| . b4) ) & ex b4 being Nat st
for b5 being Nat st b5 >= b4 holds
b3 . b5 >= 1 holds
not b2 is summable
proof end;

theorem Th36: :: BHSP_4:36
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence st ( for b4 being Nat holds b3 . b4 = b4 -root (||.b2.|| . b4) ) & b3 is convergent & lim b3 > 1 holds
not b2 is summable
proof end;

theorem Th37: :: BHSP_4:37
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds Partial_Sums ||.b2.|| is non-decreasing
proof end;

theorem Th38: :: BHSP_4:38
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Nat holds (Partial_Sums ||.b2.||) . b3 >= 0
proof end;

theorem Th39: :: BHSP_4:39
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Nat holds ||.((Partial_Sums b2) . b3).|| <= (Partial_Sums ||.b2.||) . b3
proof end;

theorem Th40: :: BHSP_4:40
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Nat holds ||.(Sum b2,b3).|| <= Sum ||.b2.||,b3 by Th39;

theorem Th41: :: BHSP_4:41
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3, b4 being Nat holds ||.(((Partial_Sums b2) . b4) - ((Partial_Sums b2) . b3)).|| <= abs (((Partial_Sums ||.b2.||) . b4) - ((Partial_Sums ||.b2.||) . b3))
proof end;

theorem Th42: :: BHSP_4:42
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3, b4 being Nat holds ||.((Sum b2,b4) - (Sum b2,b3)).|| <= abs ((Sum ||.b2.||,b4) - (Sum ||.b2.||,b3)) by Th41;

theorem Th43: :: BHSP_4:43
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3, b4 being Nat holds ||.(Sum b2,b4,b3).|| <= abs (Sum ||.b2.||,b4,b3) by Th42;

theorem Th44: :: BHSP_4:44
for b1 being RealUnitarySpace
for b2 being sequence of b1 st b1 is_Hilbert_space & b2 is absolutely_summable holds
b2 is summable
proof end;

definition
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
let c3 be Real_Sequence;
func c3 * c2 -> sequence of a1 means :Def9: :: BHSP_4:def 9
for b1 being Nat holds a4 . b1 = (a3 . b1) * (a2 . b1);
existence
ex b1 being sequence of c1 st
for b2 being Nat holds b1 . b2 = (c3 . b2) * (c2 . b2)
proof end;
uniqueness
for b1, b2 being sequence of c1 st ( for b3 being Nat holds b1 . b3 = (c3 . b3) * (c2 . b3) ) & ( for b3 being Nat holds b2 . b3 = (c3 . b3) * (c2 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines * BHSP_4:def 9 :
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence
for b4 being sequence of b1 holds
( b4 = b3 * b2 iff for b5 being Nat holds b4 . b5 = (b3 . b5) * (b2 . b5) );

theorem Th45: :: BHSP_4:45
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1
for b4 being Real_Sequence holds b4 * (b2 + b3) = (b4 * b2) + (b4 * b3)
proof end;

theorem Th46: :: BHSP_4:46
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3, b4 being Real_Sequence holds (b3 + b4) * b2 = (b3 * b2) + (b4 * b2)
proof end;

theorem Th47: :: BHSP_4:47
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3, b4 being Real_Sequence holds (b3 (#) b4) * b2 = b3 * (b4 * b2)
proof end;

theorem Th48: :: BHSP_4:48
for b1 being RealUnitarySpace
for b2 being Real
for b3 being sequence of b1
for b4 being Real_Sequence holds (b2 (#) b4) * b3 = b2 * (b4 * b3)
proof end;

theorem Th49: :: BHSP_4:49
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence holds b3 * (- b2) = (- b3) * b2
proof end;

theorem Th50: :: BHSP_4:50
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence st b3 is convergent & b2 is convergent holds
b3 * b2 is convergent
proof end;

theorem Th51: :: BHSP_4:51
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence st b3 is bounded & b2 is bounded holds
b3 * b2 is bounded
proof end;

theorem Th52: :: BHSP_4:52
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence st b3 is convergent & b2 is convergent holds
( b3 * b2 is convergent & lim (b3 * b2) = (lim b3) * (lim b2) )
proof end;

definition
let c1 be Real_Sequence;
attr a1 is Cauchy means :Def10: :: BHSP_4:def 10
for b1 being Real st b1 > 0 holds
ex b2 being Nat st
for b3, b4 being Nat st b3 >= b2 & b4 >= b2 holds
abs ((a1 . b3) - (a1 . b4)) < b1;
end;

:: deftheorem Def10 defines Cauchy BHSP_4:def 10 :
for b1 being Real_Sequence holds
( b1 is Cauchy iff for b2 being Real st b2 > 0 holds
ex b3 being Nat st
for b4, b5 being Nat st b4 >= b3 & b5 >= b3 holds
abs ((b1 . b4) - (b1 . b5)) < b2 );

notation
let c1 be Real_Sequence;
synonym c1 is_Cauchy_sequence for Cauchy c1;
end;

theorem Th53: :: BHSP_4:53
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence st b1 is_Hilbert_space & b2 is_Cauchy_sequence & b3 is_Cauchy_sequence holds
b3 * b2 is_Cauchy_sequence
proof end;

theorem Th54: :: BHSP_4:54
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence
for b4 being Nat holds (Partial_Sums ((b3 - (b3 ^\ 1)) * (Partial_Sums b2))) . b4 = ((Partial_Sums (b3 * b2)) . (b4 + 1)) - ((b3 * (Partial_Sums b2)) . (b4 + 1))
proof end;

theorem Th55: :: BHSP_4:55
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence
for b4 being Nat holds (Partial_Sums (b3 * b2)) . (b4 + 1) = ((b3 * (Partial_Sums b2)) . (b4 + 1)) - ((Partial_Sums (((b3 ^\ 1) - b3) * (Partial_Sums b2))) . b4)
proof end;

theorem Th56: :: BHSP_4:56
for b1 being RealUnitarySpace
for b2 being sequence of b1
for b3 being Real_Sequence
for b4 being Nat holds Sum (b3 * b2),(b4 + 1) = ((b3 * (Partial_Sums b2)) . (b4 + 1)) - (Sum (((b3 ^\ 1) - b3) * (Partial_Sums b2)),b4) by Th55;