:: BHSP_4 semantic presentation

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

scheme :: BHSP_4:sch 1
RecFuncExRUS{ F₁() -> RealUnitarySpace, F₂() -> Point of F₁(), F₃( Nat, Point of F₁()) -> Point of F₁() } :

ex f being Function of NAT ,the carrier of F₁() st
( f . 0 = F₂() & ( for n being Element of NAT
for x being Point of F₁() st x = f . n holds
f . (n + 1) = F₃(n,x) ) )

proof end;

definition

let X be RealUnitarySpace;
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 Nat holds it . (n + 1) = (it . n) + (seq . (n + 1)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Partial_Sums BHSP_4:def 1 :

theorem Th1: :: BHSP_4:1

for X being RealUnitarySpace
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 RealUnitarySpace
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 X being RealUnitarySpace
for a being Real
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 X being RealUnitarySpace
for a, b being Real
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 ;

end;

:: deftheorem Def2 defines summable BHSP_4:def 2 :

:: deftheorem defines Sum BHSP_4:def 3 :

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 X being RealUnitarySpace
for a being Real
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 RealUnitarySpace
for seq being sequence of X st X is_Hilbert_space holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being 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 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 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 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 Nat;
func Sum seq,n -> Point of X equals :: BHSP_4:def 4
(Partial_Sums seq) . n;
coherence ;

end;

:: deftheorem defines Sum BHSP_4:def 4 :

theorem :: BHSP_4:15

canceled;

theorem Th16: :: BHSP_4:16

for X being RealUnitarySpace
for seq being sequence of X holds Sum seq,0 = seq . 0 by Def1;

theorem Th17: :: BHSP_4:17

for X being RealUnitarySpace
for seq being sequence of X holds Sum seq,1 = (Sum seq,0) + (seq . 1)

proof end;

theorem Th18: :: BHSP_4:18

for X being RealUnitarySpace
for seq being sequence of X holds Sum seq,1 = (seq . 0) + (seq . 1)

proof end;

theorem Th19: :: BHSP_4:19

for X being RealUnitarySpace
for seq being sequence of X
for n being Nat holds Sum seq,(n + 1) = (Sum seq,n) + (seq . (n + 1)) by Def1;

theorem Th20: :: BHSP_4:20

for X being RealUnitarySpace
for seq being sequence of X
for n being Nat holds seq . (n + 1) = (Sum seq,(n + 1)) - (Sum seq,n)

proof end;

theorem :: BHSP_4:21

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 Nat;
func Sum seq,n,m -> Point of X equals :: BHSP_4:def 5
(Sum seq,n) - (Sum seq,m);
coherence ;

end;

:: deftheorem defines Sum BHSP_4:def 5 :

theorem :: BHSP_4:22

canceled;

theorem :: BHSP_4:23

for X being RealUnitarySpace
for seq being sequence of X holds Sum seq,1,0 = seq . 1

proof end;

theorem :: BHSP_4:24

for X being RealUnitarySpace
for seq being sequence of X
for n being Nat holds Sum seq,(n + 1),n = seq . (n + 1) by Th20;

theorem Th25: :: BHSP_4:25

proof end;

theorem :: BHSP_4:26

proof end;

definition

let Rseq be Real_Sequence;
let n be Nat;
func Sum Rseq,n -> Real equals :: BHSP_4:def 6
(Partial_Sums Rseq) . n;
coherence ;

end;

:: deftheorem defines Sum BHSP_4:def 6 :

definition

let Rseq be Real_Sequence;
let n, m be Nat;
func Sum Rseq,n,m -> Real equals :: BHSP_4:def 7
(Sum Rseq,n) - (Sum Rseq,m);
coherence ;

end;

:: deftheorem defines Sum BHSP_4:def 7 :

definition

let X be RealUnitarySpace;
let seq be sequence of X;
attr seq is absolutely_summable means :Def8: :: BHSP_4:def 8
||.seq.|| is summable;

end;

:: deftheorem Def8 defines absolutely_summable BHSP_4:def 8 :

theorem :: BHSP_4:27

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

for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is absolutely_summable holds
a * seq is absolutely_summable

proof end;

theorem :: BHSP_4:29

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Nat holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds
seq is absolutely_summable

proof end;

theorem :: BHSP_4:30

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being 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 Th31: :: BHSP_4:31

for X being RealUnitarySpace
for r being Real
for seq being sequence of X st r > 0 & ex m being Nat st
for n being Nat st n >= m holds
||.(seq . n).|| >= r & seq is convergent holds
lim seq <> 0. X

proof end;

theorem Th32: :: BHSP_4:32

for X being RealUnitarySpace
for seq being sequence of X st ( for n being Nat holds seq . n <> 0. X ) & ex m being Nat st
for n being Nat st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 holds
not seq is summable

proof end;

theorem :: BHSP_4:33

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Nat holds seq . n <> 0. X ) & ( for n being 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:34

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Nat holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable

proof end;

theorem :: BHSP_4:35

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Nat st
for n being Nat st n >= m holds
Rseq . n >= 1 holds
not seq is summable

proof end;

theorem :: BHSP_4:36

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable

proof end;

theorem Th37: :: BHSP_4:37

for X being RealUnitarySpace
for seq being sequence of X holds Partial_Sums ||.seq.|| is non-decreasing

proof end;

theorem :: BHSP_4:38

for X being RealUnitarySpace
for seq being sequence of X
for n being Nat holds (Partial_Sums ||.seq.||) . n >= 0

proof end;

theorem Th39: :: BHSP_4:39

for X being RealUnitarySpace
for seq being sequence of X
for n being Nat holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n

proof end;

theorem :: BHSP_4:40

for X being RealUnitarySpace
for seq being sequence of X
for n being Nat holds ||.(Sum seq,n).|| <= Sum ||.seq.||,n by Th39;

theorem Th41: :: BHSP_4:41

for X being RealUnitarySpace
for seq being sequence of X
for n, m being Nat holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n))

proof end;

theorem Th42: :: BHSP_4:42

for X being RealUnitarySpace
for seq being sequence of X
for n, m being Nat holds ||.((Sum seq,m) - (Sum seq,n)).|| <= abs ((Sum ||.seq.||,m) - (Sum ||.seq.||,n)) by Th41;

theorem :: BHSP_4:43

for X being RealUnitarySpace
for seq being sequence of X
for n, m being Nat holds ||.(Sum seq,m,n).|| <= abs (Sum ||.seq.||,m,n) by Th42;

theorem :: BHSP_4:44

for X being RealUnitarySpace
for seq being sequence of X st X is_Hilbert_space & 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 :Def9: :: BHSP_4:def 9
for n being Nat holds it . n = (Rseq . n) * (seq . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines * BHSP_4:def 9 :

theorem :: BHSP_4:45

for X being RealUnitarySpace
for seq1, seq2 being sequence of X
for Rseq being Real_Sequence holds Rseq * (seq1 + seq2) = (Rseq * seq1) + (Rseq * seq2)

proof end;

theorem :: BHSP_4:46

for X being RealUnitarySpace
for seq being sequence of X
for Rseq1, Rseq2 being Real_Sequence holds (Rseq1 + Rseq2) * seq = (Rseq1 * seq) + (Rseq2 * seq)

proof end;

theorem :: BHSP_4:47

for X being RealUnitarySpace
for seq being sequence of X
for Rseq1, Rseq2 being Real_Sequence holds (Rseq1 (#) Rseq2) * seq = Rseq1 * (Rseq2 * seq)

proof end;

theorem Th48: :: BHSP_4:48

for X being RealUnitarySpace
for a being Real
for seq being sequence of X
for Rseq being Real_Sequence holds (a (#) Rseq) * seq = a * (Rseq * seq)

proof end;

theorem :: BHSP_4:49

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence holds Rseq * (- seq) = (- Rseq) * seq

proof end;

theorem Th50: :: BHSP_4:50

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st Rseq is convergent & seq is convergent holds
Rseq * seq is convergent

proof end;

theorem :: BHSP_4:51

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st Rseq is bounded & seq is bounded holds
Rseq * seq is bounded

proof end;

theorem :: BHSP_4:52

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence 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 :Def10: :: BHSP_4:def 10
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
abs ((Rseq . n) - (Rseq . m)) < r;

end;

:: deftheorem Def10 defines Cauchy BHSP_4:def 10 :

notation

let Rseq be Real_Sequence;
synonym Rseq is_Cauchy_sequence for Cauchy Rseq;

end;

theorem :: BHSP_4:53

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence st X is_Hilbert_space & seq is_Cauchy_sequence & Rseq is_Cauchy_sequence holds
Rseq * seq is_Cauchy_sequence

proof end;

theorem Th54: :: BHSP_4:54

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence
for n being 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 Th55: :: BHSP_4:55

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence
for n being 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:56

for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence
for n being Nat holds Sum (Rseq * seq),(n + 1) = ((Rseq * (Partial_Sums seq)) . (n + 1)) - (Sum (((Rseq ^\ 1) - Rseq) * (Partial_Sums seq)),n) by Th55;