:: Banach Space of Absolute Summable Real Sequences :: by Yasumasa Suzuki, Noboru Endou and Yasunari Shidama :: :: Received August 8, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, RSSPACE, SERIES_1, TARSKI, REAL_1, SEQ_1, SEQ_2, FUNCT_1, COMPLEX1, ARYTM_1, ORDINAL2, ARYTM_3, CARD_1, XBOOLE_0, RLSUB_1, RLVECT_1, XXREAL_0, RELAT_1, VALUED_1, ALGSTR_0, CARD_3, BINOP_1, ZFMISC_1, NORMSP_1, STRUCT_0, SUPINF_2, REALSET1, PRE_TOPC, METRIC_1, NAT_1, XXREAL_2, RSSPACE3, NORMSP_0, RELAT_2, ASYMPT_1; notations TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, REALSET1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, STRUCT_0, ALGSTR_0, FUNCT_1, FUNCT_2, RELAT_1, BINOP_1, FUNCOP_1, PRE_TOPC, RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SERIES_1, PARTFUN1, FUNCSDOM, RSSPACE, XXREAL_0; constructors PARTFUN1, BINOP_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1, SEQ_2, SERIES_1, REALSET1, RLSUB_1, RSSPACE, VALUED_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, FUNCSDOM; registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, MEMBERED, REALSET1, STRUCT_0, RLVECT_1, NORMSP_1, RSSPACE, VALUED_1, FUNCT_2, SEQ_4, VALUED_0, SEQ_1, SEQ_2; 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 object holds x in it iff x in the_set_of_RealSequences & seq_id(x) is absolutely_summable; end; theorem :: RSSPACE3:1 for c be Real, seq be Real_Sequence st seq is convergent for rseq be Real_Sequence st ( for i be Nat holds rseq .i = |.seq.i-c.| ) holds rseq is convergent & lim rseq = |.lim seq-c.|; registration cluster the_set_of_l1RealSequences -> non empty; end; registration cluster the_set_of_l1RealSequences -> linearly-closed; end; registration 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 vector-distributive scalar-distributive scalar-associative scalar-unital; end; definition func l_norm -> Function of the_set_of_l1RealSequences, REAL means :: RSSPACE3:def 2 for x be object st x in the_set_of_l1RealSequences holds it.x = Sum abs seq_id x; end; registration 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:2 for l be NORMSTR st the RLSStruct of l is RealLinearSpace holds l is RealLinearSpace; theorem :: RSSPACE3:3 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:4 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:5 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:6 the carrier of l1_Space = the_set_of_l1RealSequences & ( 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:7 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 .|| = |.a.| * ||.x.||; registration cluster l1_Space -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital 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; reserve NRM for non empty RealNormSpace; reserve seq for sequence of NRM; 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; end; notation let NRM be non empty NORMSTR; let seqt be sequence of NRM; synonym seqt is Cauchy_sequence_by_Norm for seqt is CCauchy; end; theorem :: RSSPACE3:8 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:9 for vseq be sequence of l1_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent;