RSSPACE: Real Linear Space of Real Sequences

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

end;

:: deftheorem defines the_set_of_RealSequences RSSPACE:def 1 :

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 by A1, FUNCT_2:66;

end;

:: deftheorem Def2 defines seq_id RSSPACE:def 2 :

definition

::$CD 3

func Zeroseq -> Element of the_set_of_RealSequences equals :: RSSPACE:def 6
seq_const 0;

coherence by FUNCT_2:8;

end;

:: deftheorem RSSPACE:def 3 :

:: deftheorem RSSPACE:def 4 :

:: deftheorem RSSPACE:def 5 :

:: deftheorem defines Zeroseq RSSPACE:def 6 :

registration

let x be Element of the_set_of_RealSequences ;

reduce seq_id x to x;

reducibility by Def2;

end;

registration

let x be Real_Sequence;

reduce seq_id x to 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;

end;

:: deftheorem defines Linear_Space_of_RealSequences RSSPACE:def 7 :

registration

let x be Element of Linear_Space_of_RealSequences;

reduce seq_id x to x;

reducibility by Def2;

end;

registration

cluster Linear_Space_of_RealSequences -> non empty strict ;

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

proof end;

end;

:: deftheorem Def5 defines Add_ RSSPACE:def 8 :

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

proof end;

end;

:: deftheorem Def6 defines Mult_ RSSPACE:def 9 :

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;

proof end;

end;

:: deftheorem Def7 defines Zero_ RSSPACE:def 10 :

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

proof end;

proof end;

end;

:: deftheorem Def8 defines the_set_of_l2RealSequences RSSPACE:def 11 :

registration

cluster the_set_of_l2RealSequences -> non empty linearly-closed ;

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

proof end;

proof end;

end;

:: deftheorem defines l_scalar RSSPACE:def 12 :

definition end;

:: deftheorem defines l2_Space RSSPACE:def 13 :

registration

let x be Element of l2_Space;

reduce seq_id x to 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 end;