Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### Real Linear Space of Real Sequences

by
Noboru Endou,
Yasumasa Suzuki, and
Yasunari Shidama

[ Mizar article, MML identifier index ]

```environ

vocabulary RLVECT_1, FUNCT_1, ARYTM, ARYTM_1, RELAT_1, ABSVALUE, ORDINAL2,
BINOP_1, SQUARE_1, PROB_1, FUNCT_2, RLSUB_1, SEQ_1, SEQ_2, SERIES_1,
notation TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, NUMBERS, XREAL_0,
STRUCT_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, RLVECT_1,
ABSVALUE, RLSUB_1, BHSP_1, SQUARE_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1,
BINOP_1;
constructors REAL_1, NAT_1, DOMAIN_1, SQUARE_1, SEQ_2, SERIES_1, PREPOWER,
PARTFUN1, BINOP_1, RLSUB_1, BHSP_3, MEMBERED;
clusters RELSET_1, STRUCT_0, RLVECT_1, SEQ_1, BHSP_1, XREAL_0, MEMBERED;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;

begin

definition
func the_set_of_RealSequences -> non empty set means
for x being set holds x in it iff x is Real_Sequence;
end;

definition
let a be set such that
a in the_set_of_RealSequences;
func seq_id(a) -> Real_Sequence equals
a;
end;

definition
let a be set such that
a in REAL;
func R_id(a) -> Real equals
a;
end;

ex ADD be BinOp of the_set_of_RealSequences st
(for a,b being Element of the_set_of_RealSequences

ex f be Function of [: REAL, the_set_of_RealSequences :],
the_set_of_RealSequences st
for r,x be set st r in REAL & x in the_set_of_RealSequences
holds f.[r,x] = R_id(r) (#) seq_id(x);

definition
func l_add -> BinOp of the_set_of_RealSequences means
for a,b being Element of the_set_of_RealSequences holds
it.(a,b) = seq_id(a)+seq_id(b);
end;

definition
func l_mult -> Function of [: REAL, the_set_of_RealSequences :],
the_set_of_RealSequences means
for r,x be set st r in REAL & x in the_set_of_RealSequences
holds it.[r,x] = R_id(r)(#)seq_id(x);
end;

definition
func Zeroseq -> Element of the_set_of_RealSequences means
for n be Nat holds (seq_id it).n=0;
end;

for x be Real_Sequence holds seq_id x = x;

for v,w being VECTOR of
v + w = seq_id(v)+seq_id(w);

for r being Real,
v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)
holds r * v = r(#)seq_id(v);

definition
cluster RLSStruct (# the_set_of_RealSequences, Zeroseq, l_add, l_mult #) ->
Abelian;
end;

for u,v,w being VECTOR of
(u + v) + w = u + (v + w);

for v being VECTOR of
v + 0.RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) = v;

for v being VECTOR of
ex w being VECTOR of
v + w = 0.RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);

for a being Real, v,w being VECTOR of
a * (v + w) = a * v + a * w;

for a,b being Real, v being VECTOR of
(a + b) * v = a * v + b * v;

for a,b be Real, v being VECTOR of
(a * b) * v = a * (b * v);

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

definition
func Linear_Space_of_RealSequences -> RealLinearSpace equals
RLSStruct (# the_set_of_RealSequences, Zeroseq, l_add, l_mult #);
end;

definition
let X be RealLinearSpace;
let X1 be Subset of X such that
X1 is lineary-closed & X1 is non empty;
func Add_(X1,X) -> BinOp of X1 equals
(the add of X) | [:X1,X1:];
end;

definition
let X be RealLinearSpace;
let X1 be Subset of X such that
X1 is lineary-closed & X1 is non empty;
func Mult_(X1,X) -> Function of [:REAL,X1:], X1 equals
(the Mult of X) | [:REAL,X1:];
end;

definition
let X be RealLinearSpace, X1 be Subset of X such that
X1 is lineary-closed & X1 is non empty;
func Zero_(X1,X) -> Element of X1 equals
0.X;
end;

for V be RealLinearSpace, V1 be Subset of V
st V1 is lineary-closed & V1 is non empty holds
RLSStruct (# V1,Zero_(V1,V), Add_(V1,V),Mult_(V1,V) #) is Subspace of V;

definition
func the_set_of_l2RealSequences -> Subset of
Linear_Space_of_RealSequences means
it is non empty &
for x being set holds x in it iff
(x in the_set_of_RealSequences &
seq_id(x)(#)seq_id(x) is summable);
end;

the_set_of_l2RealSequences is lineary-closed &
the_set_of_l2RealSequences is non empty;

RLSStruct(# the_set_of_l2RealSequences,
Zero_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences),
Mult_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences) #)
is Subspace of Linear_Space_of_RealSequences;

RLSStruct (# the_set_of_l2RealSequences,
Zero_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences),
Mult_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences) #)
is RealLinearSpace;

the carrier of Linear_Space_of_RealSequences = the_set_of_RealSequences &
(for x be set holds
x is Element of Linear_Space_of_RealSequences
iff x is Real_Sequence )
& (for x be set holds x is VECTOR of Linear_Space_of_RealSequences
iff x is Real_Sequence )
&(for u be VECTOR of Linear_Space_of_RealSequences
holds u =seq_id(u) )
&(for u,v be VECTOR of Linear_Space_of_RealSequences
holds u+v =seq_id(u)+seq_id(v) )
&( for r be Real for u be VECTOR of Linear_Space_of_RealSequences
holds r*u =r(#)seq_id(u) );

ex f be Function of
[: the_set_of_l2RealSequences, the_set_of_l2RealSequences :], REAL st
( for x,y be set st
x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences
holds f.[x,y] = Sum(seq_id(x)(#)seq_id(y)) );

definition
func l_scalar -> Function of
[:the_set_of_l2RealSequences, the_set_of_l2RealSequences:], REAL means
(for x,y be 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)));
end;

definition
cluster UNITSTR (# the_set_of_l2RealSequences,
Zero_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences),
Mult_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences),
l_scalar #) -> non empty;
end;

definition
func l2_Space -> non empty UNITSTR equals
UNITSTR (# the_set_of_l2RealSequences,
Zero_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences),
Mult_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences),
l_scalar #);
end;

for l be UNITSTR st
RLSStruct (# the carrier of l, the Zero of l, the add of l,
the Mult of l #) is RealLinearSpace holds l is RealLinearSpace;

for rseq be Real_Sequence
st (for n be Nat holds rseq.n=0) holds
rseq is summable & Sum rseq = 0;