:: Complex Banach Space of Bounded Complex Sequences :: by Noboru Endou :: :: Received March 18, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin Lm1: for rseq being Real_Sequence for K being real number st ( for n being Element of NAT holds rseq . n <= K ) holds upper_bound (rng rseq) <= K proofend; Lm2: for rseq being Real_Sequence st rseq is bounded holds for n being Element of NAT holds rseq . n <= upper_bound (rng rseq) proofend; definition func the_set_of_BoundedComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def1: :: CSSPACE4:def 1 for x being set holds ( x in it iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ); 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 bounded ) ) 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 bounded ) ) ) & ( for x being set holds ( x in b2 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines the_set_of_BoundedComplexSequences CSSPACE4:def_1_:_ for b1 being Subset of Linear_Space_of_ComplexSequences holds ( b1 = the_set_of_BoundedComplexSequences iff for x being set holds ( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ); Lm3: for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds seq1 + seq2 is bounded proofend; Lm4: for c being Complex for seq being Complex_Sequence st seq is bounded holds c (#) seq is bounded proofend; registration cluster the_set_of_BoundedComplexSequences -> non empty ; coherence not the_set_of_BoundedComplexSequences is empty proofend; cluster the_set_of_BoundedComplexSequences -> linearly-closed ; coherence the_set_of_BoundedComplexSequences is linearly-closed proofend; end; Lm5: CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is Subspace of Linear_Space_of_ComplexSequences by CSSPACE:11; registration cluster CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is Abelian & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is add-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_zeroed & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_complementable & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is vector-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-unital ) by CSSPACE:11; end; Lm6: ( CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is Abelian & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is add-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_zeroed & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_complementable & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is vector-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-unital ) ; definition func Complex_linfty_norm -> Function of the_set_of_BoundedComplexSequences,REAL means :Def2: :: CSSPACE4:def 2 for x being set st x in the_set_of_BoundedComplexSequences holds it . x = upper_bound (rng |.(seq_id x).|); existence ex b1 being Function of the_set_of_BoundedComplexSequences,REAL st for x being set st x in the_set_of_BoundedComplexSequences holds b1 . x = upper_bound (rng |.(seq_id x).|) proofend; uniqueness for b1, b2 being Function of the_set_of_BoundedComplexSequences,REAL st ( for x being set st x in the_set_of_BoundedComplexSequences holds b1 . x = upper_bound (rng |.(seq_id x).|) ) & ( for x being set st x in the_set_of_BoundedComplexSequences holds b2 . x = upper_bound (rng |.(seq_id x).|) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines Complex_linfty_norm CSSPACE4:def_2_:_ for b1 being Function of the_set_of_BoundedComplexSequences,REAL holds ( b1 = Complex_linfty_norm iff for x being set st x in the_set_of_BoundedComplexSequences holds b1 . x = upper_bound (rng |.(seq_id x).|) ); Lm7: for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) proofend; Lm8: for seq being Complex_Sequence st seq is bounded holds |.seq.| is bounded proofend; Lm9: for seq being Complex_Sequence st |.seq.| is bounded holds seq is bounded proofend; Lm10: for seq being Complex_Sequence st seq is bounded & upper_bound (rng |.seq.|) = 0 holds for n being Element of NAT holds seq . n = 0c proofend; theorem :: CSSPACE4:1 for seq being Complex_Sequence holds ( ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) iff for n being Element of NAT holds seq . n = 0c ) by Lm7, Lm10; registration cluster CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is Abelian & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is add-associative & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is right_zeroed & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is right_complementable & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is vector-distributive & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is scalar-distributive & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is scalar-associative & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is scalar-unital ) by Lm6, CSSPACE3:2; end; definition func Complex_linfty_Space -> non empty CNORMSTR equals :: CSSPACE4:def 3 CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #); coherence CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is non empty CNORMSTR ; end; :: deftheorem defines Complex_linfty_Space CSSPACE4:def_3_:_ Complex_linfty_Space = CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #); theorem Th2: :: CSSPACE4:2 ( the carrier of Complex_linfty_Space = the_set_of_BoundedComplexSequences & ( for x being set holds ( x is VECTOR of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) ) & 0. Complex_linfty_Space = CZeroseq & ( for u being VECTOR of Complex_linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for c being Complex for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u) ) & ( for u being VECTOR of Complex_linfty_Space holds ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of Complex_linfty_Space holds ||.v.|| = upper_bound (rng |.(seq_id v).|) ) ) proofend; theorem Th3: :: CSSPACE4:3 for x, y being Point of Complex_linfty_Space for c being Complex holds ( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| ) proofend; registration cluster Complex_linfty_Space -> non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ; coherence ( Complex_linfty_Space is reflexive & Complex_linfty_Space is discerning & Complex_linfty_Space is ComplexNormSpace-like & Complex_linfty_Space is vector-distributive & Complex_linfty_Space is scalar-distributive & Complex_linfty_Space is scalar-associative & Complex_linfty_Space is scalar-unital & Complex_linfty_Space is Abelian & Complex_linfty_Space is add-associative & Complex_linfty_Space is right_zeroed & Complex_linfty_Space is right_complementable ) proofend; end; Lm11: for seq1, seq2, seq3 being Complex_Sequence holds ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) proofend; theorem Th4: :: CSSPACE4:4 for vseq being sequence of Complex_linfty_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent proofend; theorem :: CSSPACE4:5 Complex_linfty_Space is ComplexBanachSpace by Th4, CLOPBAN1:def_13; begin definition let X be non empty set ; let Y be ComplexNormSpace; let IT be Function of X, the carrier of Y; attrIT is bounded means :Def4: :: CSSPACE4:def 4 ex K being Real st ( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) ); end; :: deftheorem Def4 defines bounded CSSPACE4:def_4_:_ for X being non empty set for Y being ComplexNormSpace for IT being Function of X, the carrier of Y holds ( IT is bounded iff ex K being Real st ( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) ) ); theorem Th6: :: CSSPACE4:6 for X being non empty set for Y being ComplexNormSpace for f being Function of X, the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds f is bounded proofend; registration let X be non empty set ; let Y be ComplexNormSpace; cluster non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total bounded for Element of bool [:X, the carrier of Y:]; existence ex b1 being Function of X, the carrier of Y st b1 is bounded proofend; end; definition let X be non empty set ; let Y be ComplexNormSpace; func ComplexBoundedFunctions (X,Y) -> Subset of (ComplexVectSpace (X,Y)) means :Def5: :: CSSPACE4:def 5 for x being set holds ( x in it iff x is bounded Function of X, the carrier of Y ); existence ex b1 being Subset of (ComplexVectSpace (X,Y)) st for x being set holds ( x in b1 iff x is bounded Function of X, the carrier of Y ) proofend; uniqueness for b1, b2 being Subset of (ComplexVectSpace (X,Y)) st ( for x being set holds ( x in b1 iff x is bounded Function of X, the carrier of Y ) ) & ( for x being set holds ( x in b2 iff x is bounded Function of X, the carrier of Y ) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines ComplexBoundedFunctions CSSPACE4:def_5_:_ for X being non empty set for Y being ComplexNormSpace for b3 being Subset of (ComplexVectSpace (X,Y)) holds ( b3 = ComplexBoundedFunctions (X,Y) iff for x being set holds ( x in b3 iff x is bounded Function of X, the carrier of Y ) ); registration let X be non empty set ; let Y be ComplexNormSpace; cluster ComplexBoundedFunctions (X,Y) -> non empty ; coherence not ComplexBoundedFunctions (X,Y) is empty proofend; end; theorem Th7: :: CSSPACE4:7 for X being non empty set for Y being ComplexNormSpace holds ComplexBoundedFunctions (X,Y) is linearly-closed proofend; theorem :: CSSPACE4:8 for X being non empty set for Y being ComplexNormSpace holds CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is Subspace of ComplexVectSpace (X,Y) by Th7, CSSPACE:11; registration let X be non empty set ; let Y be ComplexNormSpace; cluster CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is Abelian & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is add-associative & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is right_zeroed & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is right_complementable & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is vector-distributive & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is scalar-distributive & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is scalar-associative & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is scalar-unital ) by Th7, CSSPACE:11; end; definition let X be non empty set ; let Y be ComplexNormSpace; func C_VectorSpace_of_BoundedFunctions (X,Y) -> ComplexLinearSpace equals :: CSSPACE4:def 6 CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #); coherence CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is ComplexLinearSpace ; end; :: deftheorem defines C_VectorSpace_of_BoundedFunctions CSSPACE4:def_6_:_ for X being non empty set for Y being ComplexNormSpace holds C_VectorSpace_of_BoundedFunctions (X,Y) = CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #); registration let X be non empty set ; let Y be ComplexNormSpace; cluster C_VectorSpace_of_BoundedFunctions (X,Y) -> strict ; coherence C_VectorSpace_of_BoundedFunctions (X,Y) is strict ; end; theorem Th9: :: CSSPACE4:9 for X being non empty set for Y being ComplexNormSpace for f, g, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) proofend; theorem Th10: :: CSSPACE4:10 for X being non empty set for Y being ComplexNormSpace for f, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) proofend; theorem Th11: :: CSSPACE4:11 for X being non empty set for Y being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) proofend; definition let X be non empty set ; let Y be ComplexNormSpace; let f be set ; assume A1: f in ComplexBoundedFunctions (X,Y) ; func modetrans (f,X,Y) -> bounded Function of X, the carrier of Y equals :Def7: :: CSSPACE4:def 7 f; coherence f is bounded Function of X, the carrier of Y by A1, Def5; end; :: deftheorem Def7 defines modetrans CSSPACE4:def_7_:_ for X being non empty set for Y being ComplexNormSpace for f being set st f in ComplexBoundedFunctions (X,Y) holds modetrans (f,X,Y) = f; definition let X be non empty set ; let Y be ComplexNormSpace; let u be Function of X, the carrier of Y; func PreNorms u -> non empty Subset of REAL equals :: CSSPACE4:def 8 { ||.(u . t).|| where t is Element of X : verum } ; coherence { ||.(u . t).|| where t is Element of X : verum } is non empty Subset of REAL proofend; end; :: deftheorem defines PreNorms CSSPACE4:def_8_:_ for X being non empty set for Y being ComplexNormSpace for u being Function of X, the carrier of Y holds PreNorms u = { ||.(u . t).|| where t is Element of X : verum } ; theorem Th12: :: CSSPACE4:12 for X being non empty set for Y being ComplexNormSpace for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above proofend; theorem :: CSSPACE4:13 for X being non empty set for Y being ComplexNormSpace for g being Function of X, the carrier of Y holds ( g is bounded iff PreNorms g is bounded_above ) proofend; definition let X be non empty set ; let Y be ComplexNormSpace; func ComplexBoundedFunctionsNorm (X,Y) -> Function of (ComplexBoundedFunctions (X,Y)),REAL means :Def9: :: CSSPACE4:def 9 for x being set st x in ComplexBoundedFunctions (X,Y) holds it . x = upper_bound (PreNorms (modetrans (x,X,Y))); existence ex b1 being Function of (ComplexBoundedFunctions (X,Y)),REAL st for x being set st x in ComplexBoundedFunctions (X,Y) holds b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) proofend; uniqueness for b1, b2 being Function of (ComplexBoundedFunctions (X,Y)),REAL st ( for x being set st x in ComplexBoundedFunctions (X,Y) holds b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in ComplexBoundedFunctions (X,Y) holds b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines ComplexBoundedFunctionsNorm CSSPACE4:def_9_:_ for X being non empty set for Y being ComplexNormSpace for b3 being Function of (ComplexBoundedFunctions (X,Y)),REAL holds ( b3 = ComplexBoundedFunctionsNorm (X,Y) iff for x being set st x in ComplexBoundedFunctions (X,Y) holds b3 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ); theorem Th14: :: CSSPACE4:14 for X being non empty set for Y being ComplexNormSpace for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f proofend; theorem Th15: :: CSSPACE4:15 for X being non empty set for Y being ComplexNormSpace for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f) proofend; definition let X be non empty set ; let Y be ComplexNormSpace; func C_NormSpace_of_BoundedFunctions (X,Y) -> non empty CNORMSTR equals :: CSSPACE4:def 10 CNORMSTR(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(ComplexBoundedFunctionsNorm (X,Y)) #); coherence CNORMSTR(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(ComplexBoundedFunctionsNorm (X,Y)) #) is non empty CNORMSTR ; end; :: deftheorem defines C_NormSpace_of_BoundedFunctions CSSPACE4:def_10_:_ for X being non empty set for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions (X,Y) = CNORMSTR(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(ComplexBoundedFunctionsNorm (X,Y)) #); theorem Th16: :: CSSPACE4:16 for X being non empty set for Y being ComplexNormSpace holds X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) proofend; theorem Th17: :: CSSPACE4:17 for X being non empty set for Y being ComplexNormSpace for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for g being bounded Function of X, the carrier of Y st g = f holds for t being Element of X holds ||.(g . t).|| <= ||.f.|| proofend; theorem :: CSSPACE4:18 for X being non empty set for Y being ComplexNormSpace for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.|| proofend; theorem Th19: :: CSSPACE4:19 for X being non empty set for Y being ComplexNormSpace for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 = ||.f.|| proofend; theorem Th20: :: CSSPACE4:20 for X being non empty set for Y being ComplexNormSpace for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) proofend; theorem Th21: :: CSSPACE4:21 for X being non empty set for Y being ComplexNormSpace for f, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds for c being Complex holds ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) proofend; theorem Th22: :: CSSPACE4:22 for X being non empty set for Y being ComplexNormSpace for f, g being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for c being Complex holds ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) proofend; theorem Th23: :: CSSPACE4:23 for X being non empty set for Y being ComplexNormSpace holds ( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like ) proofend; theorem Th24: :: CSSPACE4:24 for X being non empty set for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace proofend; registration let X be non empty set ; let Y be ComplexNormSpace; cluster C_NormSpace_of_BoundedFunctions (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ; coherence ( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like & C_NormSpace_of_BoundedFunctions (X,Y) is vector-distributive & C_NormSpace_of_BoundedFunctions (X,Y) is scalar-distributive & C_NormSpace_of_BoundedFunctions (X,Y) is scalar-associative & C_NormSpace_of_BoundedFunctions (X,Y) is scalar-unital & C_NormSpace_of_BoundedFunctions (X,Y) is Abelian & C_NormSpace_of_BoundedFunctions (X,Y) is add-associative & C_NormSpace_of_BoundedFunctions (X,Y) is right_zeroed & C_NormSpace_of_BoundedFunctions (X,Y) is right_complementable ) by Th24; end; theorem Th25: :: CSSPACE4:25 for X being non empty set for Y being ComplexNormSpace for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds ( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ) proofend; Lm12: for e being Real for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st for i being Element of NAT st k <= i holds seq . i <= e holds lim seq <= e proofend; theorem Th26: :: CSSPACE4:26 for X being non empty set for Y being ComplexNormSpace st Y is complete holds for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent proofend; theorem Th27: :: CSSPACE4:27 for X being non empty set for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace proofend; registration let X be non empty set ; let Y be ComplexBanachSpace; cluster C_NormSpace_of_BoundedFunctions (X,Y) -> non empty complete ; coherence C_NormSpace_of_BoundedFunctions (X,Y) is complete by Th27; end; begin theorem :: CSSPACE4:28 for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds seq1 + seq2 is bounded by Lm3; theorem :: CSSPACE4:29 for c being Complex for seq being Complex_Sequence st seq is bounded holds c (#) seq is bounded by Lm4; theorem :: CSSPACE4:30 for seq being Complex_Sequence holds ( seq is bounded iff |.seq.| is bounded ) by Lm8, Lm9; theorem :: CSSPACE4:31 for seq1, seq2, seq3 being Complex_Sequence holds ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) by Lm11;