:: Real Linear 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

definition
func the_set_of_RealSequences -> non empty set means :Def1: :: RSSPACE:def 1
 for x being set holds
( x in it iff x is Real_Sequence );
existence
ex b1 being non empty set st
for x being set holds
( x in b1 iff x is Real_Sequence )
proof end;
uniqueness
for b1, b2 being non empty set st ( for x being set holds
( x in b1 iff x is Real_Sequence ) ) & ( for x being set holds
( x in b2 iff x is Real_Sequence ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines the_set_of_RealSequences RSSPACE:def 1 :
for b1 being non empty set holds
( b1 = the_set_of_RealSequences iff for x being set holds
( x in b1 iff x is Real_Sequence ) );

definition
let a be set ;
assume A1: a in the_set_of_RealSequences ;
func seq_id a -> Real_Sequence equals :Def2: :: RSSPACE:def 2
a;
coherence
a is Real_Sequence by A1, Def1;
end;

:: deftheorem Def2 defines seq_id RSSPACE:def 2 :
for a being set st a in the_set_of_RealSequences holds
seq_id a = a;

definition
let a be set ;
assume A1: a in REAL ;
func R_id a -> Real equals :Def3: :: RSSPACE:def 3
a;
coherence
a is Real by A1;
end;

:: deftheorem Def3 defines R_id RSSPACE:def 3 :
for a being set st a in REAL holds
R_id a = a;

definition
func l_add -> BinOp of the_set_of_RealSequences means :Def4: :: RSSPACE:def 4
 for a, b being Element of the_set_of_RealSequences holds it . (a,b) = (seq_id a) + (seq_id b);
existence
ex b1 being BinOp of the_set_of_RealSequences st
for a, b being Element of the_set_of_RealSequences holds b1 . (a,b) = (seq_id a) + (seq_id b)
proof end;
uniqueness
for b1, b2 being BinOp of the_set_of_RealSequences st ( for a, b being Element of the_set_of_RealSequences holds b1 . (a,b) = (seq_id a) + (seq_id b) ) & ( for a, b being Element of the_set_of_RealSequences holds b2 . (a,b) = (seq_id a) + (seq_id b) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines l_add RSSPACE:def 4 :
for b1 being BinOp of the_set_of_RealSequences holds
( b1 = l_add iff for a, b being Element of the_set_of_RealSequences holds b1 . (a,b) = (seq_id a) + (seq_id b) );

definition
func l_mult -> Function of [:REAL,the_set_of_RealSequences:],the_set_of_RealSequences means :Def5: :: RSSPACE:def 5
 for r, x being set st r in REAL & x in the_set_of_RealSequences holds
it . (r,x) = (R_id r) (#) (seq_id x);
existence
ex b1 being Function of [:REAL,the_set_of_RealSequences:],the_set_of_RealSequences st
for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . (r,x) = (R_id r) (#) (seq_id x)
proof end;
uniqueness
for b1, b2 being Function of [:REAL,the_set_of_RealSequences:],the_set_of_RealSequences st ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . (r,x) = (R_id r) (#) (seq_id x) ) & ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b2 . (r,x) = (R_id r) (#) (seq_id x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines l_mult RSSPACE:def 5 :
for b1 being Function of [:REAL,the_set_of_RealSequences:],the_set_of_RealSequences holds
( b1 = l_mult iff for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . (r,x) = (R_id r) (#) (seq_id x) );

definition
func Zeroseq -> Element of the_set_of_RealSequences means :Def6: :: RSSPACE:def 6
 for n being Element of NAT holds (seq_id it) . n = 0 ;
existence
ex b1 being Element of the_set_of_RealSequences st
for n being Element of NAT holds (seq_id b1) . n = 0
proof end;
uniqueness
for b1, b2 being Element of the_set_of_RealSequences st ( for n being Element of NAT holds (seq_id b1) . n = 0 ) & ( for n being Element of NAT holds (seq_id b2) . n = 0 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Zeroseq RSSPACE:def 6 :
for b1 being Element of the_set_of_RealSequences holds
( b1 = Zeroseq iff for n being Element of NAT holds (seq_id b1) . n = 0 );

theorem Th1: :: RSSPACE:1
for x being Real_Sequence holds seq_id x = x
proof end;

theorem :: RSSPACE:2
for v, w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds v + w = (seq_id v) + (seq_id w) by Def4;

theorem Th3: :: RSSPACE:3
for r being Real
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds r * v = r (#) (seq_id v)
proof end;

registration
cluster RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) -> Abelian ;
coherence
RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is Abelian
proof end;
end;

theorem Th4: :: RSSPACE:4
for u, v, w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (u + v) + w = u + (v + w)
proof end;

theorem Th5: :: RSSPACE:5
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds v + (0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)) = v
proof end;

theorem Th6: :: RSSPACE:6
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) ex w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) st v + w = 0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)
proof end;

theorem Th7: :: RSSPACE:7
for a being Real
for v, w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds a * (v + w) = (a * v) + (a * w)
proof end;

theorem Th8: :: RSSPACE:8
for a, b being Real
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a + b) * v = (a * v) + (b * v)
proof end;

theorem Th9: :: RSSPACE:9
for a, b being Real
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a * b) * v = a * (b * v)
proof end;

theorem Th10: :: RSSPACE:10
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds 1 * v = v
proof end;

definition
func Linear_Space_of_RealSequences -> RLSStruct equals :: RSSPACE:def 7
 RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);
correctness
coherence
RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is RLSStruct ;
;
end;

:: deftheorem defines Linear_Space_of_RealSequences RSSPACE:def 7 :
Linear_Space_of_RealSequences = RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);

registration
cluster Linear_Space_of_RealSequences -> non empty strict ;
coherence
( Linear_Space_of_RealSequences is strict & not Linear_Space_of_RealSequences is empty ) ;
end;

registration
cluster Linear_Space_of_RealSequences -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( Linear_Space_of_RealSequences is Abelian & Linear_Space_of_RealSequences is add-associative & Linear_Space_of_RealSequences is right_zeroed & Linear_Space_of_RealSequences is right_complementable & Linear_Space_of_RealSequences is vector-distributive & Linear_Space_of_RealSequences is scalar-distributive & Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )
proof end;
end;

definition
let X be RealLinearSpace;
let X1 be Subset of X;
assume B1: ( X1 is linearly-closed & not X1 is empty ) ;
func Add_ (X1,X) -> BinOp of X1 equals :Def8: :: RSSPACE:def 8
 the addF of X || X1;
correctness
coherence
the addF of X || X1 is BinOp of X1;
proof end;
end;

:: deftheorem Def8 defines Add_ RSSPACE:def 8 :
for X being RealLinearSpace
for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds
Add_ (X1,X) = the addF of X || X1;

definition
let X be RealLinearSpace;
let X1 be Subset of X;
assume B1: ( X1 is linearly-closed & not X1 is empty ) ;
func Mult_ (X1,X) -> Function of [:REAL,X1:],X1 equals :Def9: :: RSSPACE:def 9
 the Mult of X | [:REAL,X1:];
correctness
coherence
the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1;
proof end;
end;

:: deftheorem Def9 defines Mult_ RSSPACE:def 9 :
for X being RealLinearSpace
for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds
Mult_ (X1,X) = the Mult of X | [:REAL,X1:];

definition
let X be RealLinearSpace;
let X1 be Subset of X;
assume A1: ( X1 is linearly-closed & not X1 is empty ) ;
func Zero_ (X1,X) -> Element of X1 equals :Def10: :: RSSPACE:def 10
 0. X;
correctness
coherence
0. X is Element of X1;
proof end;
end;

:: deftheorem Def10 defines Zero_ RSSPACE:def 10 :
for X being RealLinearSpace
for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds
Zero_ (X1,X) = 0. X;

theorem Th11: :: RSSPACE:11
for V being RealLinearSpace
for V1 being Subset of V st V1 is linearly-closed & not V1 is empty holds
RLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V
proof end;

definition
func the_set_of_l2RealSequences -> Subset of Linear_Space_of_RealSequences means :Def11: :: RSSPACE:def 11
 for x being set holds
( x in it iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) );
existence
ex b1 being Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) )
proof end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_RealSequences st ( for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines the_set_of_l2RealSequences RSSPACE:def 11 :
for b1 being Subset of Linear_Space_of_RealSequences holds
( b1 = the_set_of_l2RealSequences iff for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) );

registration
cluster the_set_of_l2RealSequences -> non empty linearly-closed ;
coherence
( the_set_of_l2RealSequences is linearly-closed & not the_set_of_l2RealSequences is empty )
proof end;
end;

theorem :: RSSPACE:12
RLSStruct(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)) #) is Subspace of Linear_Space_of_RealSequences by Th11;

theorem Th13: :: RSSPACE:13
RLSStruct(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)) #) is RealLinearSpace by Th11;

theorem :: RSSPACE:14
( the carrier of Linear_Space_of_RealSequences = the_set_of_RealSequences & ( for x being set holds
( x is VECTOR of Linear_Space_of_RealSequences iff x is Real_Sequence ) ) & ( for u being VECTOR of Linear_Space_of_RealSequences holds u = seq_id u ) & ( for u, v being VECTOR of Linear_Space_of_RealSequences holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of Linear_Space_of_RealSequences holds r * u = r (#) (seq_id u) ) ) by Def1, Def2, Def4, Th3;

definition
func l_scalar -> Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL means :: RSSPACE:def 12
 for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
it . (x,y) = Sum ((seq_id x) (#) (seq_id y));
existence
ex b1 being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL st
for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) (seq_id y))
proof end;
uniqueness
for b1, b2 being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL st ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) ) & ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b2 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines l_scalar RSSPACE:def 12 :
for b1 being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL holds
( b1 = l_scalar iff for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) );

registration
cluster UNITSTR(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),l_scalar #) -> non empty ;
coherence
not UNITSTR(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),l_scalar #) is empty ;
end;

definition
func l2_Space -> non empty UNITSTR equals :: RSSPACE:def 13
 UNITSTR(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),l_scalar #);
coherence
UNITSTR(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),l_scalar #) is non empty UNITSTR ;
end;

:: deftheorem defines l2_Space RSSPACE:def 13 :
l2_Space = UNITSTR(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),l_scalar #);

theorem Th15: :: RSSPACE:15
for l being RLSStruct st RLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is RealLinearSpace holds
l is RealLinearSpace
proof end;

theorem :: RSSPACE:16
for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds
( rseq is summable & Sum rseq = 0 )
proof end;

theorem :: RSSPACE:17
for rseq being Real_Sequence st ( for n being Element of NAT holds 0 <= rseq . n ) & rseq is summable & Sum rseq = 0 holds
for n being Element of NAT holds rseq . n = 0
proof end;

registration
cluster l2_Space -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( l2_Space is Abelian & l2_Space is add-associative & l2_Space is right_zeroed & l2_Space is right_complementable & l2_Space is vector-distributive & l2_Space is scalar-distributive & l2_Space is scalar-associative & l2_Space is scalar-unital ) by Th13, Th15;
end;