:: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama

::

:: Received April 3, 2003

:: Copyright (c) 2003-2018 Association of Mizar Users

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

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

proof end;

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 ) & ( x = 0. l2_Space implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

for a being Real holds

( ( x .|. x = 0 implies x = 0. l2_Space ) & ( x = 0. l2_Space implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

proof end;

Lm1: for rseq being Real_Sequence st ( for n being Nat holds 0 <= rseq . n ) holds

( ( for n being Nat holds 0 <= (Partial_Sums rseq) . n ) & ( for n being Nat holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Nat holds rseq . n <= Sum rseq ) ) ) )

proof end;

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

proof end;

Lm3: for e being Real

for seq being Real_Sequence st seq is convergent & ex k being Nat st

for i being Nat st k <= i holds

seq . i <= e holds

lim seq <= e

proof end;

Lm4: for c being Real

for seq being Real_Sequence st seq is convergent holds

for rseq being Real_Sequence st ( for i being Nat holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds

( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) )

proof end;

Lm5: for c being Real

for seq, seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds

for rseq being Real_Sequence st ( for i being Nat holds rseq . i = (((seq . i) - c) * ((seq . i) - c)) + (seq1 . i) ) holds

( rseq is convergent & lim rseq = (((lim seq) - c) * ((lim seq) - c)) + (lim seq1) )

proof end;

registration

ex b_{1} being RealUnitarySpace st b_{1} is complete
end;

cluster V82() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like complete for RealUnitarySpace;

existence ex b

proof end;

theorem :: RSSPACE2:3

for r being Real_Sequence st ( for n being Nat holds 0 <= r . n ) holds

( ( for n being Nat holds 0 <= (Partial_Sums r) . n ) & ( for n being Nat holds r . n <= (Partial_Sums r) . n ) & ( r is summable implies ( ( for n being Nat holds (Partial_Sums r) . n <= Sum r ) & ( for n being Nat holds r . n <= Sum r ) ) ) ) by Lm1;

( ( for n being Nat holds 0 <= (Partial_Sums r) . n ) & ( for n being Nat holds r . n <= (Partial_Sums r) . n ) & ( r is summable implies ( ( for n being Nat holds (Partial_Sums r) . n <= Sum r ) & ( for n being Nat holds r . n <= Sum r ) ) ) ) by Lm1;

theorem :: RSSPACE2:4

theorem :: RSSPACE2:5

theorem :: RSSPACE2:6

theorem :: RSSPACE2:7