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


definition
func the_set_of_RealSequences -> non empty set equals :: RSSPACE:def 1
 Funcs (NAT,REAL);
coherence
Funcs (NAT,REAL) is non empty set ;
end;

:: deftheorem defines the_set_of_RealSequences RSSPACE:def 1 :
the_set_of_RealSequences = Funcs (NAT,REAL);

definition
let a be object ;
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, FUNCT_2:66;
end;

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

definition
::$CD 3
func Zeroseq -> Element of the_set_of_RealSequences equals :: RSSPACE:def 6
 seq_const 0;
coherence
seq_const 0 is Element of the_set_of_RealSequences by FUNCT_2:8;
end;

:: deftheorem RSSPACE:def 3 :
canceled;

:: deftheorem RSSPACE:def 4 :
canceled;

:: deftheorem RSSPACE:def 5 :
canceled;

:: deftheorem defines Zeroseq RSSPACE:def 6 :
Zeroseq = seq_const 0;

registration
let x be Element of the_set_of_RealSequences ;
reduce seq_id x to x;
reducibility
seq_id x = x by Def2;
end;

registration
let x be Real_Sequence;
reduce seq_id x to x;
reducibility
seq_id x = x
proof end;
end;

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

definition
func Linear_Space_of_RealSequences -> strict RLSStruct equals :: RSSPACE:def 7
 RealVectSpace NAT;
coherence
RealVectSpace NAT is strict RLSStruct ;
end;

:: deftheorem defines Linear_Space_of_RealSequences RSSPACE:def 7 :
Linear_Space_of_RealSequences = RealVectSpace NAT;

registration
let x be Element of Linear_Space_of_RealSequences;
reduce seq_id x to x;
reducibility
seq_id x = x by Def2;
end;

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

theorem :: RSSPACE:2
for v, w being VECTOR of Linear_Space_of_RealSequences holds v + w = (seq_id v) + (seq_id w)
proof end;

theorem Th3: :: RSSPACE:3
for r being Real
for v being VECTOR of Linear_Space_of_RealSequences holds r * v = r (#) (seq_id v)
proof end;

registration
cluster Linear_Space_of_RealSequences -> right_complementable strict 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 ) ;
end;

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

:: deftheorem Def5 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 A1: ( X1 is linearly-closed & not X1 is empty ) ;
func Mult_ (X1,X) -> Function of [:REAL,X1:],X1 equals :Def6: :: 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 Def6 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 :Def7: :: RSSPACE:def 10
 0. X;
correctness
coherence
0. X is Element of X1;
proof end;
end;

:: deftheorem Def7 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 :: RSSPACE:4
for n being object holds (seq_id Zeroseq) . n = 0
proof end;

theorem :: RSSPACE:5
for f being Element of the_set_of_RealSequences st ( for n being Nat holds (seq_id f) . n = 0 ) holds
f = Zeroseq
proof end;

theorem :: RSSPACE:6
canceled;

theorem :: RSSPACE:7
canceled;

theorem :: RSSPACE:8
canceled;

theorem :: RSSPACE:9
canceled;

theorem :: RSSPACE:10
canceled;

::$CT 5
theorem Th4: :: 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 :Def8: :: RSSPACE:def 11
 for x being object 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 object 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 object holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) & ( for x being object 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 Def8 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 object 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 Th4;

theorem Th6: :: 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 Th4;

theorem :: RSSPACE:14
canceled;

::$CT
definition
func l_scalar -> Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL means :: RSSPACE:def 12
 for x, y being object 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 object 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 object 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 object 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 object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) );

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

registration
let x be Element of l2_Space;
reduce seq_id x to x;
reducibility
seq_id x = x
proof end;
end;

theorem Th7: :: 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 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 Nat holds 0 <= rseq . n ) & rseq is summable & Sum rseq = 0 holds
for n being 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 Th6, Th7;
end;