Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

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