:: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama

::

:: Received April 3, 2003

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

:: deftheorem defines the_set_of_RealSequences RSSPACE:def 1 :

the_set_of_RealSequences = Funcs (NAT,REAL);

the_set_of_RealSequences = Funcs (NAT,REAL);

definition

let a be object ;

assume A1: a in the_set_of_RealSequences ;

coherence

a is Real_Sequence by A1, FUNCT_2:66;

end;
assume A1: a in the_set_of_RealSequences ;

coherence

a is Real_Sequence by A1, FUNCT_2:66;

:: deftheorem Def2 defines seq_id RSSPACE:def 2 :

for a being object st a in the_set_of_RealSequences holds

seq_id a = a;

for a being object st a in the_set_of_RealSequences holds

seq_id a = a;

registration
end;

:: deftheorem defines Linear_Space_of_RealSequences RSSPACE:def 7 :

Linear_Space_of_RealSequences = RealVectSpace NAT;

Linear_Space_of_RealSequences = RealVectSpace NAT;

registration
end;

registration

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

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

definition

let X be RealLinearSpace;

let X1 be Subset of X;

assume A1: ( X1 is linearly-closed & not X1 is empty ) ;

correctness

coherence

the addF of X || X1 is BinOp of X1;

end;
let X1 be Subset of X;

assume A1: ( X1 is linearly-closed & not X1 is empty ) ;

correctness

coherence

the addF of X || X1 is BinOp of X1;

proof 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;

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

coherence

the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1;

end;
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 the Mult of X | [:REAL,X1:];

coherence

the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1;

proof 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:];

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

correctness

coherence

0. X is Element of X1;

end;
let X1 be Subset of X;

assume A1: ( X1 is linearly-closed & not X1 is empty ) ;

correctness

coherence

0. X is Element of X1;

proof 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;

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:5

for f being Element of the_set_of_RealSequences st ( for n being Nat holds (seq_id f) . n = 0 ) holds

f = Zeroseq

f = Zeroseq

proof end;

::$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

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

ex b_{1} being Subset of Linear_Space_of_RealSequences st

for x being object holds

( x in b_{1} iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) )

for b_{1}, b_{2} being Subset of Linear_Space_of_RealSequences st ( for x being object holds

( x in b_{1} iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) & ( for x being object holds

( x in b_{2} iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) holds

b_{1} = b_{2}
end;

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 for x being object holds

( x in it iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def8 defines the_set_of_l2RealSequences RSSPACE:def 11 :

for b_{1} being Subset of Linear_Space_of_RealSequences holds

( b_{1} = the_set_of_l2RealSequences iff for x being object holds

( x in b_{1} iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) );

for b

( b

( x in b

registration

coherence

( the_set_of_l2RealSequences is linearly-closed & not the_set_of_l2RealSequences is empty )

end;
( the_set_of_l2RealSequences is linearly-closed & not the_set_of_l2RealSequences is empty )

proof end;

theorem :: RSSPACE:12

::$CT

definition

ex b_{1} 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

b_{1} . (x,y) = Sum ((seq_id x) (#) (seq_id y))

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (x,y) = Sum ((seq_id x) (#) (seq_id y)) ) holds

b_{1} = b_{2}
end;

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

ex b

for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines l_scalar RSSPACE:def 12 :

for b_{1} being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL holds

( b_{1} = l_scalar iff for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds

b_{1} . (x,y) = Sum ((seq_id x) (#) (seq_id y)) );

for b

( b

b

definition

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;

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

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 ;

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

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

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 )

( 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

for n being Nat holds rseq . n = 0

proof end;

registration

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

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;