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

### Banach Space of Absolute Summable Real Sequences

by
Yasumasa Suzuki,
Noboru Endou, and
Yasunari Shidama

Received August 8, 2003

MML identifier: RSSPACE3
[ Mizar article, MML identifier index ]

```environ

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

begin :: l1_Space:The Space of Absolute Summable Real Sequences

definition
func the_set_of_l1RealSequences -> Subset of
Linear_Space_of_RealSequences means
:: RSSPACE3:def 1
for x being set holds x in it
iff
(x in the_set_of_RealSequences & seq_id(x) is absolutely_summable);
end;

definition
cluster the_set_of_l1RealSequences -> non empty;
end;

theorem :: RSSPACE3:1
the_set_of_l1RealSequences is lineary-closed;

theorem :: RSSPACE3:2
RLSStruct (# the_set_of_l1RealSequences,
Zero_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
Add_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
Mult_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences) #)
is Subspace of Linear_Space_of_RealSequences;

definition
cluster RLSStruct (# the_set_of_l1RealSequences,
Zero_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
Add_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
Mult_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences) #)
-> Abelian add-associative right_zeroed right_complementable
RealLinearSpace-like;
end;

theorem :: RSSPACE3:3
RLSStruct (# the_set_of_l1RealSequences,
Zero_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
Add_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
Mult_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences) #)
is RealLinearSpace;

definition
func l_norm -> Function of the_set_of_l1RealSequences, REAL means
:: RSSPACE3:def 2
for x be set st x in the_set_of_l1RealSequences holds
it.x = Sum(abs(seq_id(x)));
end;

definition let X be non empty set,
Z be Element of X, A be BinOp of X,
M be Function of [:REAL, X:], X,
N be Function of X, REAL;
cluster NORMSTR (# X, Z, A, M, N #) -> non empty;
end;

theorem :: RSSPACE3:4
for l be NORMSTR st RLSStruct (# the carrier of l, the Zero of l,
the add of l, the Mult of l #)
is RealLinearSpace holds l is RealLinearSpace;

theorem :: RSSPACE3:5
for rseq be Real_Sequence
st (for n be Nat holds rseq.n=0) holds
rseq is absolutely_summable & Sum(abs(rseq))=0;

theorem :: RSSPACE3:6
for rseq be Real_Sequence st
( rseq is absolutely_summable & Sum(abs(rseq))=0 ) holds
for n be Nat holds rseq.n =0;

theorem :: RSSPACE3:7
NORMSTR (# the_set_of_l1RealSequences,
Zero_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
Add_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
Mult_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
l_norm #) is RealLinearSpace;

definition
func l1_Space -> non empty NORMSTR equals
:: RSSPACE3:def 3
NORMSTR (# the_set_of_l1RealSequences,
Zero_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
Add_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
Mult_(the_set_of_l1RealSequences,Linear_Space_of_RealSequences),
l_norm #);
end;

begin :: l1_Space is Banach

theorem :: RSSPACE3:8
the carrier of l1_Space = the_set_of_l1RealSequences &
( for x be set holds
x is Element of l1_Space
iff x is Real_Sequence & seq_id(x) is absolutely_summable ) &
( for x be set holds
x is VECTOR of l1_Space
iff x is Real_Sequence & seq_id(x) is absolutely_summable ) &
0.l1_Space = Zeroseq &
( for u be VECTOR of l1_Space holds u =seq_id(u) ) &
( for u,v be VECTOR of l1_Space holds u+v =seq_id(u)+seq_id(v) ) &
( for r be Real for u be VECTOR of l1_Space holds r*u =r(#)seq_id(u) ) &
( for u be VECTOR of l1_Space holds
-u = -seq_id(u) & seq_id(-u) = -seq_id(u) ) &
( for u,v be VECTOR of l1_Space holds u-v =seq_id(u)-seq_id(v) ) &
( for v be VECTOR of l1_Space holds seq_id(v) is absolutely_summable ) &
( for v be VECTOR of l1_Space holds ||.v.|| = Sum(abs(seq_id(v))) );

theorem :: RSSPACE3:9
for x, y being Point of l1_Space, a be Real holds
( ||.x.|| = 0 iff x = 0.l1_Space ) &
0 <= ||.x.|| &
||.x+y.|| <= ||.x.|| +  ||.y.|| &
||.(a*x).|| = abs(a) * ||.x.||;

definition
cluster l1_Space -> RealNormSpace-like RealLinearSpace-like
Abelian add-associative right_zeroed right_complementable;
end;

definition let X be non empty NORMSTR, x, y be Point of X;
func dist(x,y) -> Real equals
:: RSSPACE3:def 4
||.x - y.||;
end;

definition
let NRM be non empty NORMSTR;
let seqt be sequence of NRM;
attr seqt is CCauchy means
:: RSSPACE3:def 5
for r1 be Real st r1 > 0 ex k1 be Nat st
for n1, m1 be Nat st n1 >= k1 & m1 >= k1 holds
dist(seqt.n1, seqt.m1) < r1;
synonym seqt is Cauchy_sequence_by_Norm;
end;

reserve NRM for non empty RealNormSpace;
reserve seq for sequence of NRM;

theorem :: RSSPACE3:10
seq is Cauchy_sequence_by_Norm iff for r be Real st r > 0
ex k be Nat st for n, m be Nat st
n >= k & m >= k holds ||.(seq.n) - (seq.m).|| < r;

theorem :: RSSPACE3:11
for vseq be sequence of l1_Space st vseq is Cauchy_sequence_by_Norm
holds vseq is convergent;
```

Back to top