:: Banach Space of Absolute Summable Complex Sequences :: by Noboru Endou :: :: Received February 24, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin definition func the_set_of_l1ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def1: :: CSSPACE3:def 1 for x being set holds ( x in it iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ); existence ex b1 being Subset of Linear_Space_of_ComplexSequences st for x being set holds ( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) proofend; uniqueness for b1, b2 being Subset of Linear_Space_of_ComplexSequences st ( for x being set holds ( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) ) & ( for x being set holds ( x in b2 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines the_set_of_l1ComplexSequences CSSPACE3:def_1_:_ for b1 being Subset of Linear_Space_of_ComplexSequences holds ( b1 = the_set_of_l1ComplexSequences iff for x being set holds ( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) ); theorem Th1: :: CSSPACE3:1 for c being Complex for seq being Complex_Sequence for rseq being Real_Sequence st seq is convergent & ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| ) holds ( rseq is convergent & lim rseq = |.((lim seq) - c).| ) proofend; registration cluster the_set_of_l1ComplexSequences -> non empty ; coherence not the_set_of_l1ComplexSequences is empty proofend; end; registration cluster the_set_of_l1ComplexSequences -> linearly-closed ; coherence the_set_of_l1ComplexSequences is linearly-closed proofend; end; Lm1: 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)) #) is Subspace of Linear_Space_of_ComplexSequences by CSSPACE:11; 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)) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( 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)) #) is Abelian & 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)) #) is add-associative & 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)) #) is right_zeroed & 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)) #) is right_complementable & 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)) #) is vector-distributive & 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)) #) is scalar-distributive & 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)) #) is scalar-associative & 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)) #) is scalar-unital ) by CSSPACE:11; end; definition func cl_norm -> Function of the_set_of_l1ComplexSequences,REAL means :Def2: :: CSSPACE3:def 2 for x being set st x in the_set_of_l1ComplexSequences holds it . x = Sum |.(seq_id x).|; existence ex b1 being Function of the_set_of_l1ComplexSequences,REAL st for x being set st x in the_set_of_l1ComplexSequences holds b1 . x = Sum |.(seq_id x).| proofend; uniqueness for b1, b2 being Function of the_set_of_l1ComplexSequences,REAL st ( for x being set st x in the_set_of_l1ComplexSequences holds b1 . x = Sum |.(seq_id x).| ) & ( for x being set st x in the_set_of_l1ComplexSequences holds b2 . x = Sum |.(seq_id x).| ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines cl_norm CSSPACE3:def_2_:_ for b1 being Function of the_set_of_l1ComplexSequences,REAL holds ( b1 = cl_norm iff for x being set st x in the_set_of_l1ComplexSequences holds b1 . x = Sum |.(seq_id x).| ); registration let X be non empty set ; let Z be Element of X; let A be BinOp of X; let M be Function of [:COMPLEX,X:],X; let N be Function of X,REAL; cluster CNORMSTR(# X,Z,A,M,N #) -> non empty ; coherence not CNORMSTR(# X,Z,A,M,N #) is empty ; end; theorem :: CSSPACE3:2 for l being CNORMSTR st CLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is ComplexLinearSpace holds l is ComplexLinearSpace by CSSPACE:79; theorem Th3: :: CSSPACE3:3 for cseq being Complex_Sequence st ( for n being Element of NAT holds cseq . n = 0c ) holds ( cseq is absolutely_summable & Sum |.cseq.| = 0 ) proofend; theorem Th4: :: CSSPACE3:4 for cseq being Complex_Sequence st cseq is absolutely_summable & Sum |.cseq.| = 0 holds for n being Element of NAT holds cseq . n = 0c proofend; Lm2: 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)) #) is ComplexLinearSpace ; 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 #); coherence 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 #) is non empty CNORMSTR ; end; :: deftheorem defines Complex_l1_Space CSSPACE3:def_3_:_ Complex_l1_Space = 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 #); theorem Th5: :: CSSPACE3:5 Complex_l1_Space is ComplexLinearSpace by Lm2, CSSPACE:79; begin theorem Th6: :: CSSPACE3:6 ( the carrier of Complex_l1_Space = the_set_of_l1ComplexSequences & ( for x being 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 being VECTOR of Complex_l1_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_l1_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for p being Complex for u being VECTOR of Complex_l1_Space holds p * u = p (#) (seq_id u) ) & ( for u being VECTOR of Complex_l1_Space holds ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_l1_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_l1_Space holds seq_id v is absolutely_summable ) & ( for v being VECTOR of Complex_l1_Space holds ||.v.|| = Sum |.(seq_id v).| ) ) proofend; theorem Th7: :: CSSPACE3:7 for x, y being Point of Complex_l1_Space for p being Complex holds ( ( ||.x.|| = 0 implies x = 0. Complex_l1_Space ) & ( x = 0. Complex_l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(p * x).|| = |.p.| * ||.x.|| ) proofend; registration cluster Complex_l1_Space -> non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ; coherence ( Complex_l1_Space is reflexive & Complex_l1_Space is discerning & Complex_l1_Space is ComplexNormSpace-like & Complex_l1_Space is vector-distributive & Complex_l1_Space is scalar-distributive & Complex_l1_Space is scalar-associative & Complex_l1_Space is scalar-unital & Complex_l1_Space is Abelian & Complex_l1_Space is add-associative & Complex_l1_Space is right_zeroed & Complex_l1_Space is right_complementable ) proofend; end; Lm3: for c being Complex for seq being Complex_Sequence for seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds ( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) ) proofend; definition let X be non empty CNORMSTR ; let x, y be Point of X; func dist (x,y) -> Real equals :: CSSPACE3:def 4 ||.(x - y).||; coherence ||.(x - y).|| is Real ; end; :: deftheorem defines dist CSSPACE3:def_4_:_ for X being non empty CNORMSTR for x, y being Point of X holds dist (x,y) = ||.(x - y).||; definition let CNRM be non empty CNORMSTR ; let seqt be sequence of CNRM; attrseqt is CCauchy means :Def5: :: CSSPACE3:def 5 for r1 being Real st r1 > 0 holds ex k1 being Element of NAT st for n1, m1 being Element of NAT st n1 >= k1 & m1 >= k1 holds dist ((seqt . n1),(seqt . m1)) < r1; end; :: deftheorem Def5 defines CCauchy CSSPACE3:def_5_:_ for CNRM being non empty CNORMSTR for seqt being sequence of CNRM holds ( seqt is CCauchy iff for r1 being Real st r1 > 0 holds ex k1 being Element of NAT st for n1, m1 being Element of NAT st n1 >= k1 & m1 >= k1 holds dist ((seqt . n1),(seqt . m1)) < r1 ); notation let CNRM be non empty CNORMSTR ; let seq be sequence of CNRM; synonym Cauchy_sequence_by_Norm seq for CCauchy ; end; theorem Th8: :: CSSPACE3:8 for NRM being ComplexNormSpace for seq being sequence of NRM holds ( seq is Cauchy_sequence_by_Norm iff for r being Real st r > 0 holds ex k being Element of NAT st for n, m being Element of NAT st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r ) proofend; theorem :: CSSPACE3:9 for vseq being sequence of Complex_l1_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent proofend;