:: Hilbert Space of Real Sequences
:: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama
::
:: Received April 3, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

theorem Th1: :: RSSPACE2:1
( the carrier of l2_Space = the_set_of_l2RealSequences & ( for x being set holds
( x is VECTOR of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) ) & 0. l2_Space = Zeroseq & ( for u being VECTOR of l2_Space holds u = seq_id u ) & ( for u, v being VECTOR of l2_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of l2_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v, w being VECTOR of l2_Space holds
( (seq_id v) (#) (seq_id w) is summable & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum ((seq_id v) (#) (seq_id w)) ) ) ) )
proofend;

theorem Th2: :: RSSPACE2:2
for x, y, z being Point of l2_Space
for a being Real holds
( ( x .|. x = 0 implies x = 0. l2_Space ) &amp; ( x = 0. l2_Space implies x .|. x = 0 ) &amp; 0 <= x .|. x &amp; x .|. y = y .|. x &amp; (x + y) .|. z = (x .|. z) + (y .|. z) &amp; (a * x) .|. y = a * (x .|. y) )
proofend;

registration
cluster l2_Space  ->  RealUnitarySpace-like ;
coherence
 l2_Space is RealUnitarySpace-like by Th2, BHSP_1:def_2;
end;

Lm1:  for rseq being Real_Sequence st ( for n being Element of NAT holds 0 <= rseq . n ) holds
( ( for n being Element of NAT holds 0 <= (Partial_Sums rseq) . n ) &amp; ( for n being Element of NAT holds rseq . n <= (Partial_Sums rseq) . n ) &amp; ( rseq is summable implies ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) &amp; ( for n being Element of NAT holds rseq . n <= Sum rseq ) ) ) )
proofend;

Lm2:  ( ( for x, y being Real holds (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y) ) &amp; ( for x, y being Real holds x * x <= ((2 * (x - y)) * (x - y)) + ((2 * y) * y) ) )
proofend;

Lm3:  for e being Real
for seq being Real_Sequence st seq is convergent &amp; ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
proofend;

Lm4:  for c being Real
for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds
( rseq is convergent &amp; lim rseq = ((lim seq) - c) * ((lim seq) - c) )
proofend;

Lm5:  for c being Real
for seq, seq1 being Real_Sequence st seq is convergent &amp; seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (((seq . i) - c) * ((seq . i) - c)) + (seq1 . i) ) holds
( rseq is convergent &amp; lim rseq = (((lim seq) - c) * ((lim seq) - c)) + (lim seq1) )
proofend;

registration
cluster l2_Space  ->  complete ;
coherence
 l2_Space is complete
proofend;
end;

registration
clusterV78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like complete for UNITSTR ;
existence
 ex b1 being RealUnitarySpace st b1 is complete
proofend;
end;

definition
mode RealHilbertSpace is complete RealUnitarySpace;
end;

begin

theorem :: RSSPACE2:3
for r being Real_Sequence st ( for n being Element of NAT holds 0 <= r . n ) holds
( ( for n being Element of NAT holds 0 <= (Partial_Sums r) . n ) &amp; ( for n being Element of NAT holds r . n <= (Partial_Sums r) . n ) &amp; ( r is summable implies ( ( for n being Element of NAT holds (Partial_Sums r) . n <= Sum r ) &amp; ( for n being Element of NAT holds r . n <= Sum r ) ) ) ) by Lm1;

theorem :: RSSPACE2:4
( ( for x, y being Real holds (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y) ) &amp; ( for x, y being Real holds x * x <= ((2 * (x - y)) * (x - y)) + ((2 * y) * y) ) ) by Lm2;

theorem :: RSSPACE2:5
for e being Real
for s being Real_Sequence st s is convergent &amp; ex k being Element of NAT st
for i being Element of NAT st k <= i holds
s . i <= e holds
lim s <= e by Lm3;

theorem :: RSSPACE2:6
for c being Real
for s being Real_Sequence st s is convergent holds
for r being Real_Sequence st ( for i being Element of NAT holds r . i = ((s . i) - c) * ((s . i) - c) ) holds
( r is convergent &amp; lim r = ((lim s) - c) * ((lim s) - c) ) by Lm4;

theorem :: RSSPACE2:7
for c being Real
for s, s1 being Real_Sequence st s is convergent &amp; s1 is convergent holds
for r being Real_Sequence st ( for i being Element of NAT holds r . i = (((s . i) - c) * ((s . i) - c)) + (s1 . i) ) holds
( r is convergent &amp; lim r = (((lim s) - c) * ((lim s) - c)) + (lim s1) ) by Lm5;