:: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama

::

:: Received April 3, 2003

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

begin

definition

ex b_{1} being non empty set st

for x being set holds

( x in b_{1} iff x is Real_Sequence )

for b_{1}, b_{2} being non empty set st ( for x being set holds

( x in b_{1} iff x is Real_Sequence ) ) & ( for x being set holds

( x in b_{2} iff x is Real_Sequence ) ) holds

b_{1} = b_{2}
end;

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

( x in it iff x is Real_Sequence );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines the_set_of_RealSequences RSSPACE:def 1 :

for b_{1} being non empty set holds

( b_{1} = the_set_of_RealSequences iff for x being set holds

( x in b_{1} iff x is Real_Sequence ) );

for b

( b

( x in b

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

for a being set st a in the_set_of_RealSequences holds

seq_id a = a;

definition

ex b_{1} being BinOp of the_set_of_RealSequences st

for a, b being Element of the_set_of_RealSequences holds b_{1} . (a,b) = (seq_id a) + (seq_id b)

for b_{1}, b_{2} being BinOp of the_set_of_RealSequences st ( for a, b being Element of the_set_of_RealSequences holds b_{1} . (a,b) = (seq_id a) + (seq_id b) ) & ( for a, b being Element of the_set_of_RealSequences holds b_{2} . (a,b) = (seq_id a) + (seq_id b) ) holds

b_{1} = b_{2}
end;

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 for a, b being Element of the_set_of_RealSequences holds it . (a,b) = (seq_id a) + (seq_id b);

ex b

for a, b being Element of the_set_of_RealSequences holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines l_add RSSPACE:def 4 :

for b_{1} being BinOp of the_set_of_RealSequences holds

( b_{1} = l_add iff for a, b being Element of the_set_of_RealSequences holds b_{1} . (a,b) = (seq_id a) + (seq_id b) );

for b

( b

definition

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

b_{1} . (r,x) = (R_id r) (#) (seq_id x)

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

b_{1} . (r,x) = (R_id r) (#) (seq_id x) ) & ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds

b_{2} . (r,x) = (R_id r) (#) (seq_id x) ) holds

b_{1} = b_{2}
end;

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

ex b

for r, x being set st r in REAL & x in the_set_of_RealSequences holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines l_mult RSSPACE:def 5 :

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

( b_{1} = l_mult iff for r, x being set st r in REAL & x in the_set_of_RealSequences holds

b_{1} . (r,x) = (R_id r) (#) (seq_id x) );

for b

( b

b

definition

ex b_{1} being Element of the_set_of_RealSequences st

for n being Element of NAT holds (seq_id b_{1}) . n = 0

for b_{1}, b_{2} being Element of the_set_of_RealSequences st ( for n being Element of NAT holds (seq_id b_{1}) . n = 0 ) & ( for n being Element of NAT holds (seq_id b_{2}) . n = 0 ) holds

b_{1} = b_{2}
end;

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 for n being Element of NAT holds (seq_id it) . n = 0 ;

ex b

for n being Element of NAT holds (seq_id b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines Zeroseq RSSPACE:def 6 :

for b_{1} being Element of the_set_of_RealSequences holds

( b_{1} = Zeroseq iff for n being Element of NAT holds (seq_id b_{1}) . n = 0 );

for b

( b

theorem :: RSSPACE:2

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)

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

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)

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)

for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a * b) * v = a * (b * v)

proof end;

definition

coherence

RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is RLSStruct ;

;

end;

func Linear_Space_of_RealSequences -> RLSStruct equals :: RSSPACE:def 7

RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);

correctness RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);

coherence

RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is RLSStruct ;

;

:: deftheorem defines Linear_Space_of_RealSequences RSSPACE:def 7 :

Linear_Space_of_RealSequences = RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);

Linear_Space_of_RealSequences = RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);

registration

coherence

( Linear_Space_of_RealSequences is strict & not Linear_Space_of_RealSequences is empty ) ;

end;
( Linear_Space_of_RealSequences is strict & not Linear_Space_of_RealSequences is empty ) ;

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

definition

let X be RealLinearSpace;

let X1 be Subset of X;

assume B1: ( 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 B1: ( X1 is linearly-closed & not X1 is empty ) ;

correctness

coherence

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

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

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

coherence

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

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

coherence

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

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

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

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

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

( x in b_{1} iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) & ( for x being set 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 :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 for x being set holds

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

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def11 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 set 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

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;

( 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

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

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

ex b

for x, y being set 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 set 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

registration

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;

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 ;

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

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

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 )

( 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

for n being Element of 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 Th13, Th15;

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 Th13, Th15;