:: Banach Algebra of Complex-Valued Continuous Functionals and Space of :: Complex-valued Continuous Functionals with Bounded Support :: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama :: :: Received May 30, 2011 :: Copyright (c) 2011-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 STRUCT_0, FUNCOP_1, NUMBERS, PRE_TOPC, ORDINAL2, SUBSET_1, RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1, ARYTM_3, ARYTM_1, COMPLEX1, ALGSTR_0, FUNCSDOM, REAL_1, FUNCT_2, C0SP1, IDEAL_1, VALUED_1, MESFUNC1, RSSPACE, BINOP_1, SUPINF_2, GROUP_1, REALSET1, ZFMISC_1, XXREAL_2, XXREAL_0, NORMSP_1, CFUNCDOM, CLVECT_1, VECTSP_1, RELAT_2, CLOPBAN2, METRIC_1, XCMPLX_0, RCOMP_1, CONNSP_2, CC0SP1, CC0SP2, RLVECT_1, XXREAL_1, NAT_1, CLOPBAN1, SEQ_2, RSSPACE3, LOPBAN_2, SEQFUNC, REWRITE1, CSSPACE4, PARTFUN1, PRE_POLY, RLSUB_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, COMPLEX1, XXREAL_2, REALSET1, VALUED_1, COMSEQ_2, SEQ_2, RCOMP_1, CFDIFF_1, SEQFUNC, PRE_POLY, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, GROUP_1, VECTSP_1, COMPTS_1, NORMSP_0, CONNSP_2, PSCOMP_1, IDEAL_1, CLVECT_1, CSSPACE, CSSPACE3, CLOPBAN1, CFUNCDOM, CLOPBAN2, NCFCONT1, C0SP1, CC0SP1; constructors REAL_1, REALSET1, IDEAL_1, C0SP1, PARTFUN3, BINOP_2, SEQ_4, MEASURE6, CSSPACE3, COMSEQ_3, CFDIFF_1, CC0SP1, WEIERSTR, PSCOMP_1, NCFCONT1, SEQFUNC, INTEGRA2, PRE_POLY, C0SP2, COMSEQ_2, TOPS_2; registrations XBOOLE_0, SUBSET_1, STRUCT_0, XREAL_0, REALSET1, NUMBERS, MEMBERED, VECTSP_1, VECTSP_2, VALUED_0, XXREAL_0, FUNCT_2, VALUED_1, COMPLEX1, CFUNCDOM, XCMPLX_0, PRE_TOPC, CC0SP1, PSCOMP_1, ORDINAL1, CLOPBAN2, COMPTS_1, RELSET_1, JORDAN5A, XXREAL_2, WAYBEL_2; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin :: Banach Algebra of Complex-Valued Continuous Functionals definition let X be TopStruct; let f be Function of the carrier of X,COMPLEX; attr f is continuous means :: CC0SP2:def 1 :: PSCOMP_1:def 25 for Y being Subset of COMPLEX st Y is closed holds f " Y is closed; end; definition let X be 1-sorted, y be Complex; func X --> y -> Function of the carrier of X,COMPLEX equals :: CC0SP2:def 2 (the carrier of X) --> y; end; theorem :: CC0SP2:1 for X being non empty TopSpace for y being Complex for f being Function of the carrier of X,COMPLEX st f=X --> y holds f is continuous; registration let X be non empty TopSpace, y be Complex; cluster X --> y -> continuous; end; registration let X be non empty TopSpace; cluster continuous for Function of the carrier of X,COMPLEX; end; theorem :: CC0SP2:2 for X being non empty TopSpace, f being Function of the carrier of X,COMPLEX holds ( f is continuous iff for Y being Subset of COMPLEX st Y is open holds f " Y is open ); theorem :: CC0SP2:3 :: LMcont for X being non empty TopSpace for f be Function of the carrier of X,COMPLEX holds (f is continuous iff for x being Point of X for V being Subset of COMPLEX st f.x in V & V is open holds ex W being Subset of X st (x in W & W is open & f.:W c= V)); theorem :: CC0SP2:4 for X being non empty TopSpace for f,g being continuous Function of the carrier of X,COMPLEX holds f+g is continuous Function of the carrier of X,COMPLEX; theorem :: CC0SP2:5 for X being non empty TopSpace for a being Complex for f being continuous Function of the carrier of X,COMPLEX holds a(#)f is continuous Function of the carrier of X,COMPLEX; theorem :: CC0SP2:6 for X being non empty TopSpace, f,g be continuous Function of the carrier of X,COMPLEX holds f-g is continuous Function of the carrier of X,COMPLEX; theorem :: CC0SP2:7 for X being non empty TopSpace, f,g be continuous Function of the carrier of X,COMPLEX holds f(#)g is continuous Function of the carrier of X,COMPLEX; theorem :: CC0SP2:8 for X being non empty TopSpace for f being continuous Function of the carrier of X,COMPLEX holds ( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous); definition let X be non empty TopSpace; func CContinuousFunctions(X) -> Subset of CAlgebra the carrier of X equals :: CC0SP2:def 3 the set of all f where f is continuous Function of the carrier of X,COMPLEX; end; registration let X be non empty TopSpace; cluster CContinuousFunctions(X) -> non empty; end; registration let X be non empty TopSpace; cluster CContinuousFunctions X -> Cadditively-linearly-closed multiplicatively-closed; end; definition let X be non empty TopSpace; func C_Algebra_of_ContinuousFunctions X -> ComplexAlgebra equals :: CC0SP2:def 4 ComplexAlgebraStr (# CContinuousFunctions X, mult_(CContinuousFunctions X,CAlgebra the carrier of X), Add_(CContinuousFunctions X,CAlgebra the carrier of X), Mult_(CContinuousFunctions X,CAlgebra the carrier of X), One_(CContinuousFunctions X,CAlgebra the carrier of X), Zero_(CContinuousFunctions X,CAlgebra the carrier of X) #); end; theorem :: CC0SP2:9 for X be non empty TopSpace holds C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X; registration let X be non empty TopSpace; cluster C_Algebra_of_ContinuousFunctions X -> strict non empty; end; registration let X be non empty TopSpace; cluster C_Algebra_of_ContinuousFunctions X -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital commutative associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative; end; theorem :: CC0SP2:10 for X being non empty TopSpace for F, G, H being VECTOR of (C_Algebra_of_ContinuousFunctions X) for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds ( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) ); theorem :: CC0SP2:11 for X being non empty TopSpace for F, G being VECTOR of (C_Algebra_of_ContinuousFunctions X) for f, g being Function of the carrier of X,COMPLEX for a being Complex st f = F & g = G holds ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ); theorem :: CC0SP2:12 for X being non empty TopSpace for F, G, H being VECTOR of (C_Algebra_of_ContinuousFunctions X) for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds ( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) ); theorem :: CC0SP2:13 for X being non empty TopSpace holds 0.(C_Algebra_of_ContinuousFunctions X) = X --> 0c; theorem :: CC0SP2:14 for X being non empty TopSpace holds 1_(C_Algebra_of_ContinuousFunctions X) = X --> 1r; theorem :: CC0SP2:15 for A being ComplexAlgebra for A1, A2 being ComplexSubAlgebra of A st the carrier of A1 c= the carrier of A2 holds A1 is ComplexSubAlgebra of A2; theorem :: CC0SP2:16 for X being non empty compact TopSpace holds C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of C_Algebra_of_BoundedFunctions the carrier of X; definition let X be non empty compact TopSpace; func CContinuousFunctionsNorm X -> Function of (CContinuousFunctions X),REAL equals :: CC0SP2:def 5 (ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X); end; definition let X be non empty compact TopSpace; func C_Normed_Algebra_of_ContinuousFunctions X -> Normed_Complex_AlgebraStr equals :: CC0SP2:def 6 Normed_Complex_AlgebraStr(# (CContinuousFunctions X), (mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))), (Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))), (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))), (One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))), (Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))), (CContinuousFunctionsNorm X) #); end; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> non empty strict; end; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> unital; end; theorem :: CC0SP2:17 for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative; end; theorem :: CC0SP2:18 for X being non empty compact TopSpace for F being Point of C_Normed_Algebra_of_ContinuousFunctions X holds (Mult_(CContinuousFunctions X,CAlgebra the carrier of X)).(1r,F) = F; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> vector-distributive scalar-distributive scalar-associative scalar-unital; end; theorem :: CC0SP2:19 for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X is ComplexLinearSpace; theorem :: CC0SP2:20 for X being non empty compact TopSpace holds X --> 0 = 0.(C_Normed_Algebra_of_ContinuousFunctions X); theorem :: CC0SP2:21 for X being non empty compact TopSpace for F being Point of C_Normed_Algebra_of_ContinuousFunctions X holds 0 <= ||.F.||; theorem :: CC0SP2:22 for X being non empty compact TopSpace for f, g, h being Function of the carrier of X,COMPLEX for F, G, H being Point of C_Normed_Algebra_of_ContinuousFunctions X st f = F & g = G & h = H holds (H = F+G iff for x being Element of X holds h.x=(f.x)+(g.x)); theorem :: CC0SP2:23 for a being Complex for X being non empty compact TopSpace for f, g being Function of the carrier of X,COMPLEX for F, G being Point of C_Normed_Algebra_of_ContinuousFunctions X st f = F & g = G holds (G = a*F iff for x being Element of X holds g.x = a*(f.x)); theorem :: CC0SP2:24 for X being non empty compact TopSpace for f, g, h being Function of the carrier of X,COMPLEX for F, G, H being Point of C_Normed_Algebra_of_ContinuousFunctions X st f = F & g = G & h = H holds ( H= F*G iff for x being Element of X holds h.x = (f.x)*(g.x)); theorem :: CC0SP2:25 for X being non empty compact TopSpace holds ||.0.C_Normed_Algebra_of_ContinuousFunctions X.|| = 0; theorem :: CC0SP2:26 for X being non empty compact TopSpace for F being Point of C_Normed_Algebra_of_ContinuousFunctions X holds ||.F.|| = 0 implies F = 0.C_Normed_Algebra_of_ContinuousFunctions X; theorem :: CC0SP2:27 for a being Complex for X being non empty compact TopSpace for F being Point of C_Normed_Algebra_of_ContinuousFunctions X holds ||.(a*F).|| = |.a.|*||.F.||; theorem :: CC0SP2:28 for X being non empty compact TopSpace for F, G being Point of C_Normed_Algebra_of_ContinuousFunctions X holds ||.(F + G).|| <= ||.F.|| + ||.G.||; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> discerning reflexive ComplexNormSpace-like; end; theorem :: CC0SP2:29 for X being non empty compact TopSpace for f, g, h being Function of the carrier of X,COMPLEX for F, G, H being Point of C_Normed_Algebra_of_ContinuousFunctions X st f = F & g = G & h = H holds ( H = F - G iff for x being Element of X holds h.x = (f.x)-(g.x)); theorem :: CC0SP2:30 for X being ComplexBanachSpace for Y being Subset of X for seq being sequence of X st Y is closed & rng seq c= Y & seq is CCauchy holds seq is convergent & lim seq in Y; theorem :: CC0SP2:31 for X being non empty compact TopSpace for Y being Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = CContinuousFunctions X holds Y is closed; theorem :: CC0SP2:32 for X being non empty compact TopSpace for seq being sequence of (C_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds seq is convergent; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> complete; end; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> Banach_Algebra-like; end; :: Some properties of support theorem :: CC0SP2:33 for X being non empty TopSpace for f,g being Function of the carrier of X,COMPLEX holds support(f+g) c= support(f) \/ support(g); theorem :: CC0SP2:34 for X being non empty TopSpace for a be Complex,f be Function of the carrier of X,COMPLEX holds support(a(#)f) c= support(f); theorem :: CC0SP2:35 for X being non empty TopSpace for f,g be Function of the carrier of X,COMPLEX holds support(f(#)g) c= support(f) \/ support(g); :: Space of Complex-Valued Continuous Functionals with bounded support definition let X be non empty TopSpace; func CC_0_Functions(X) -> non empty Subset of ComplexVectSpace the carrier of X equals :: CC0SP2:def 7 { f where f is Function of the carrier of X,COMPLEX : f is continuous & ex Y be non empty Subset of X st( Y is compact & (for A being Subset of X st A=support(f) holds Cl(A) is Subset of Y))}; end; theorem :: CC0SP2:36 for X being non empty TopSpace holds CC_0_Functions(X) is non empty Subset of CAlgebra the carrier of X; theorem :: CC0SP2:37 for X being non empty TopSpace for W be non empty Subset of CAlgebra the carrier of X st W= CC_0_Functions X holds W is Cadditively-linearly-closed; theorem :: CC0SP2:38 for X being non empty TopSpace holds CC_0_Functions X is add-closed; theorem :: CC0SP2:39 for X being non empty TopSpace holds CC_0_Functions X is linearly-closed; registration let X being non empty TopSpace; cluster CC_0_Functions X -> non empty linearly-closed; end; theorem :: CC0SP2:40 :: CSSPACE:13 for V being ComplexLinearSpace for V1 being Subset of V st V1 is linearly-closed & not V1 is empty holds CLSStruct(# V1,(Zero_(V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V ; theorem :: CC0SP2:41 for X being non empty TopSpace holds CLSStruct (# CC_0_Functions X, Zero_(CC_0_Functions X, ComplexVectSpace(the carrier of X)), Add_(CC_0_Functions X, ComplexVectSpace(the carrier of X)), Mult_(CC_0_Functions X, ComplexVectSpace(the carrier of X)) #) is Subspace of ComplexVectSpace(the carrier of X); definition let X be non empty TopSpace; func C_VectorSpace_of_C_0_Functions X -> ComplexLinearSpace equals :: CC0SP2:def 8 CLSStruct (# CC_0_Functions X, Zero_(CC_0_Functions X, ComplexVectSpace(the carrier of X)), Add_(CC_0_Functions X, ComplexVectSpace(the carrier of X)), Mult_(CC_0_Functions X, ComplexVectSpace(the carrier of X)) #); end; theorem :: CC0SP2:42 for X be non empty TopSpace for x being set st x in CC_0_Functions(X) holds x in ComplexBoundedFunctions the carrier of X; definition let X be non empty TopSpace; func CC_0_FunctionsNorm X -> Function of CC_0_Functions(X),REAL equals :: CC0SP2:def 9 (ComplexBoundedFunctionsNorm the carrier of X)|(CC_0_Functions(X)); end; definition let X be non empty TopSpace; func C_Normed_Space_of_C_0_Functions X -> CNORMSTR equals :: CC0SP2:def 10 CNORMSTR (# CC_0_Functions X, Zero_(CC_0_Functions X, ComplexVectSpace(the carrier of X)), Add_(CC_0_Functions X, ComplexVectSpace(the carrier of X)), Mult_(CC_0_Functions X, ComplexVectSpace(the carrier of X)), CC_0_FunctionsNorm X #); end; registration let X be non empty TopSpace; cluster C_Normed_Space_of_C_0_Functions X -> strict non empty; end; theorem :: CC0SP2:43 for X be non empty TopSpace for x be set st x in CC_0_Functions(X) holds x in CContinuousFunctions X; theorem :: CC0SP2:44 for X be non empty TopSpace holds 0.C_VectorSpace_of_C_0_Functions X = X --> 0; theorem :: CC0SP2:45 for X be non empty TopSpace holds 0.C_Normed_Space_of_C_0_Functions X = X --> 0; theorem :: CC0SP2:46 for a be Complex for X be non empty TopSpace for F,G be Point of C_Normed_Space_of_C_0_Functions(X) holds (||.F.|| = 0 iff F = 0.C_Normed_Space_of_C_0_Functions(X) ) & ||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||; registration let X be non empty TopSpace; cluster C_Normed_Space_of_C_0_Functions(X) -> reflexive discerning ComplexNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; end; theorem :: CC0SP2:47 for X be non empty TopSpace holds C_Normed_Space_of_C_0_Functions(X) is ComplexNormSpace;