:: Banach Space of Absolute Summable Complex Sequences :: by Noboru Endou :: :: Received February 24, 2004 :: Copyright (c) 2004-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, CSSPACE, RSSPACE, SERIES_1, TARSKI, XCMPLX_0, COMSEQ_1, SEQ_1, SEQ_2, FUNCT_1, COMPLEX1, ARYTM_1, ORDINAL2, FUNCOP_1, ARYTM_3, XBOOLE_0, RLSUB_1, RLVECT_1, CARD_1, XXREAL_0, RELAT_1, VALUED_1, CLVECT_1, ALGSTR_0, CARD_3, BINOP_1, ZFMISC_1, STRUCT_0, SUPINF_2, NORMSP_1, REALSET1, PRE_TOPC, METRIC_1, REAL_1, NAT_1, RSSPACE3, XXREAL_2, CSSPACE3, NORMSP_0, RELAT_2; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XREAL_0, XCMPLX_0, COMPLEX1, NAT_1, STRUCT_0, ALGSTR_0, RELAT_1, BINOP_1, REALSET1, DOMAIN_1, PARTFUN1, FUNCT_1, XXREAL_0, FUNCT_2, FUNCOP_1, PRE_TOPC, RLVECT_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, NORMSP_0, CLVECT_1, CSSPACE; constructors BINOP_1, FUNCOP_1, REAL_1, COMSEQ_2, COMSEQ_3, REALSET1, CSSPACE, SEQ_2, RELSET_1, CFUNCDOM; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, COMSEQ_2, REALSET1, STRUCT_0, CLVECT_1, CSSPACE, VALUED_1, VALUED_0, XCMPLX_0, SEQ_2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin :: Complex_l1_Space:The Space of Absolute Summable Complex Sequences definition func the_set_of_l1ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :: CSSPACE3:def 1 for x being object holds x in it iff x in the_set_of_ComplexSequences & seq_id(x) is absolutely_summable; end; theorem :: CSSPACE3:1 for c be Complex, seq be Complex_Sequence, rseq be Real_Sequence st seq is convergent & ( for i be Nat holds rseq.i = |.(seq.i-c).| ) holds rseq is convergent & lim rseq = |.(lim seq-c).|; registration cluster the_set_of_l1ComplexSequences -> non empty; end; registration cluster the_set_of_l1ComplexSequences -> linearly-closed; end; registration cluster CLSStruct (# the_set_of_l1ComplexSequences, Zero_( the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Add_( the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Mult_( the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; end; definition func cl_norm -> Function of the_set_of_l1ComplexSequences, REAL means :: CSSPACE3:def 2 for x be object st x in the_set_of_l1ComplexSequences holds it.x = Sum |.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 [:COMPLEX, X:], X, N be Function of X, REAL; cluster CNORMSTR (# X, Z, A, M, N #) -> non empty; end; theorem :: CSSPACE3:2 for l be CNORMSTR st the CLSStruct of l is ComplexLinearSpace holds l is ComplexLinearSpace; theorem :: CSSPACE3:3 for cseq be Complex_Sequence st (for n be Nat holds cseq.n=0c) holds cseq is absolutely_summable & Sum |.cseq.| = 0; definition func Complex_l1_Space -> non empty CNORMSTR equals :: CSSPACE3:def 3 CNORMSTR (# the_set_of_l1ComplexSequences, Zero_(the_set_of_l1ComplexSequences, Linear_Space_of_ComplexSequences), Add_(the_set_of_l1ComplexSequences, Linear_Space_of_ComplexSequences), Mult_(the_set_of_l1ComplexSequences, Linear_Space_of_ComplexSequences), cl_norm #); end; ::$CT theorem :: CSSPACE3:5 Complex_l1_Space is ComplexLinearSpace; begin :: Complex_l1_Space is Banach theorem :: CSSPACE3:6 the carrier of Complex_l1_Space = the_set_of_l1ComplexSequences & ( for x be set holds x is VECTOR of Complex_l1_Space iff x is Complex_Sequence & seq_id x is absolutely_summable ) & 0.Complex_l1_Space = CZeroseq & ( for u be VECTOR of Complex_l1_Space holds u =seq_id u ) & ( for u,v be VECTOR of Complex_l1_Space holds u+v =seq_id(u)+seq_id(v) ) & ( for p be Complex for u be VECTOR of Complex_l1_Space holds p*u =p(#)seq_id(u) ) & ( for u be VECTOR of Complex_l1_Space holds -u = -seq_id u & seq_id(-u) = -seq_id(u) ) & ( for u,v be VECTOR of Complex_l1_Space holds u-v =seq_id(u)-seq_id v ) & ( for v be VECTOR of Complex_l1_Space holds seq_id v is absolutely_summable ) & for v be VECTOR of Complex_l1_Space holds ||.v.|| = Sum |.seq_id v.|; theorem :: CSSPACE3:7 for x, y being Point of Complex_l1_Space, p be Complex holds ( ||.x.|| = 0 iff x = 0.Complex_l1_Space ) & 0 <= ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| & ||. p*x .|| = |.p.| * ||.x.||; registration cluster Complex_l1_Space -> reflexive discerning ComplexNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; end; definition let X be non empty CNORMSTR, x, y be Point of X; func dist(x,y) -> Real equals :: CSSPACE3:def 4 ||.x - y.||; end; definition let CNRM be non empty CNORMSTR; let seqt be sequence of CNRM; attr seqt is CCauchy means :: CSSPACE3: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 CNRM be non empty CNORMSTR; let seq be sequence of CNRM; synonym seq is Cauchy_sequence_by_Norm for seq is CCauchy; end; reserve NRM for non empty ComplexNormSpace; reserve seq for sequence of NRM; theorem :: CSSPACE3: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 :: CSSPACE3:9 for vseq be sequence of Complex_l1_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent;