begin
:: 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 ) );
:: deftheorem Def2 defines seq_id RSSPACE:def 2 :
for a being set st a in the_set_of_RealSequences holds
seq_id a = a;
:: deftheorem Def3 defines R_id RSSPACE:def 3 :
for a being set st a in REAL holds
R_id a = a;
theorem Th1:
theorem Th2:
:: 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:
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)
by Th2;
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
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) );
:: 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 Th3:
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem defines Linear_Space_of_RealSequences RSSPACE:def 7 :
Linear_Space_of_RealSequences = RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);
:: 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;
:: 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:];
:: 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 Th13:
:: 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 ) ) );
theorem
canceled;
theorem
theorem Th16:
theorem
theorem Th18:
definition
func l_scalar -> Function of
[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],
REAL means
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))
by Th18;
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
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
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 Th19:
theorem
theorem