:: Banach Algebra of Bounded Complex-Valued Functionals :: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama :: :: Received November 20, 2010 :: Copyright (c) 2010-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, RLVECT_1, 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, REWRITE1, NAT_1, RSSPACE3, SEQ_2, PARTFUN1, SEQ_1, LOPBAN_1, SEQ_4, CFUNCDOM, CLVECT_1, VECTSP_1, RELAT_2, CC0SP1, XCMPLX_0, CLOPBAN2, LOPBAN_2, METRIC_1, COMSEQ_1, CSSPACE4; 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, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, COMPLEX1, XXREAL_2, REALSET1, VALUED_1, SEQ_1, SEQ_2, SEQ_4, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, GROUP_1, VECTSP_1, NORMSP_0, IDEAL_1, CLVECT_1, CFUNCDOM, CLOPBAN2, C0SP1, CLOPBAN1, COMSEQ_1, CSSPACE3, COMSEQ_2; constructors REAL_1, REALSET1, COMPLEX1, IDEAL_1, C0SP1, PARTFUN3, BINOP_2, TOPMETR, SEQ_4, MEASURE6, CLOPBAN2, CSSPACE3, COMSEQ_2; registrations XBOOLE_0, SUBSET_1, STRUCT_0, XREAL_0, REALSET1, ALGSTR_0, NUMBERS, ORDINAL1, MEMBERED, VECTSP_1, VECTSP_2, VALUED_0, C0SP1, XXREAL_0, FUNCT_2, VALUED_1, RFUNCT_1, COMPLEX1, FUNCOP_1, CFUNCDOM, CLVECT_1, XCMPLX_0, COMSEQ_2, CLOPBAN2, RELSET_1, SEQ_2; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin :: Banach Algebra of Bounded Complex-Valued Functionals definition let V be ComplexAlgebra; mode ComplexSubAlgebra of V -> ComplexAlgebra means :: CC0SP1:def 1 the carrier of it c= the carrier of V & the addF of it = (the addF of V)||the carrier of it & the multF of it = (the multF of V)||the carrier of it & the Mult of it = (the Mult of V) | [:COMPLEX,the carrier of it:] & 1.it = 1.V & 0.it = 0.V; end; theorem :: CC0SP1:1 for X being non empty set, V being ComplexAlgebra, V1 being non empty Subset of V, d1,d2 being Element of X, A being BinOp of X, M being Function of [:X,X:],X, MR being Function of [:COMPLEX,X:],X st (V1 = X & d1 = 0.V & d2 = 1.V & A = (the addF of V)||V1 & M = (the multF of V)||V1 & MR = (the Mult of V) | [:COMPLEX,V1:] & V1 is having-inverse) holds ComplexAlgebraStr(#X,M,A,MR,d2,d1#) is ComplexSubAlgebra of V; registration let V be ComplexAlgebra; cluster strict for ComplexSubAlgebra of V; end; definition let V be ComplexAlgebra, V1 be Subset of V; attr V1 is Cadditively-linearly-closed means :: CC0SP1:def 2 V1 is add-closed having-inverse & for a be Complex, v be Element of V st v in V1 holds a * v in V1; end; definition let V be ComplexAlgebra, V1 be Subset of V such that V1 is Cadditively-linearly-closed non empty; func Mult_(V1,V) -> Function of [:COMPLEX,V1:], V1 equals :: CC0SP1:def 3 (the Mult of V) | [:COMPLEX,V1:]; end; definition let X be non empty set; func ComplexBoundedFunctions(X) -> non empty Subset of CAlgebra X equals :: CC0SP1:def 4 { f where f is Function of X,COMPLEX : f|X is bounded }; end; registration let X be non empty set; cluster CAlgebra X -> scalar-unital; end; registration let X be non empty set; cluster ComplexBoundedFunctions(X) -> Cadditively-linearly-closed multiplicatively-closed; end; registration let V be ComplexAlgebra; cluster Cadditively-linearly-closed multiplicatively-closed for non empty Subset of V; end; definition let V be non empty CLSStruct; attr V is scalar-mult-cancelable means :: CC0SP1:def 5 for a be Complex, v be Element of V st a*v=0.V holds a=0 or v=0.V; end; theorem :: CC0SP1:2 for V being ComplexAlgebra, V1 being Cadditively-linearly-closed multiplicatively-closed non empty Subset of V holds ComplexAlgebraStr(# V1,mult_(V1,V), Add_(V1,V), Mult_(V1,V), One_(V1,V), Zero_(V1,V) #) is ComplexSubAlgebra of V; theorem :: CC0SP1:3 for V be ComplexAlgebra, V1 be ComplexSubAlgebra of V holds ( for v1,w1 be Element of V1, v,w be Element of V st v1=v & w1=w holds v1+w1=v+w ) & ( for v1,w1 be Element of V1, v,w be Element of V st v1=v & w1=w holds v1*w1=v*w ) & ( for v1 be Element of V1, v be Element of V, a be Complex st v1=v holds a*v1=a*v ) & 1_V1 = 1_V & 0.V1=0.V; definition let X be non empty set; func C_Algebra_of_BoundedFunctions X -> ComplexAlgebra equals :: CC0SP1:def 6 ComplexAlgebraStr (# ComplexBoundedFunctions(X), mult_(ComplexBoundedFunctions(X),CAlgebra(X)), Add_(ComplexBoundedFunctions(X),CAlgebra(X)), Mult_(ComplexBoundedFunctions(X),CAlgebra(X)), One_(ComplexBoundedFunctions(X),CAlgebra(X)), Zero_(ComplexBoundedFunctions(X),CAlgebra(X)) #); end; theorem :: CC0SP1:4 for X being non empty set holds C_Algebra_of_BoundedFunctions(X) is ComplexSubAlgebra of CAlgebra(X); registration let X be non empty set; cluster C_Algebra_of_BoundedFunctions(X) -> vector-distributive scalar-unital; end; theorem :: CC0SP1:5 for X being non empty set, F, G, H being VECTOR of C_Algebra_of_BoundedFunctions(X), f, g, h being Function of X,COMPLEX st f=F & g=G & h=H holds ( H = F+G iff (for x be Element of X holds h.x = (f.x) + (g.x)) ); theorem :: CC0SP1:6 for X being non empty set, a being Complex, F, G being VECTOR of C_Algebra_of_BoundedFunctions(X), f, g being Function of X,COMPLEX st f=F & g=G holds ( G = a*F iff for x be Element of X holds g.x = a*(f.x) ); theorem :: CC0SP1:7 for X being non empty set, F, G, H being VECTOR of C_Algebra_of_BoundedFunctions(X), f, g, h being Function of X,COMPLEX st f=F & g=G & h=H holds ( H = F*G iff for x be Element of X holds h.x = (f.x)*(g.x)); theorem :: CC0SP1:8 for X being non empty set holds 0.C_Algebra_of_BoundedFunctions X = X -->0; theorem :: CC0SP1:9 for X being non empty set holds 1_C_Algebra_of_BoundedFunctions X = X --> 1r; definition let X be non empty set, F be object; assume F in ComplexBoundedFunctions(X); func modetrans(F,X) -> Function of X,COMPLEX means :: CC0SP1:def 7 it = F & it|X is bounded; end; definition let X be non empty set, f be Function of X,COMPLEX; func PreNorms f -> non empty Subset of REAL equals :: CC0SP1:def 8 the set of all |.f.x.| where x is Element of X ; end; theorem :: CC0SP1:10 for X being non empty set, f being Function of X,COMPLEX st f | X is bounded holds PreNorms f is bounded_above; theorem :: CC0SP1:11 for X being non empty set, f being Function of X,COMPLEX holds f|X is bounded iff PreNorms f is bounded_above; definition let X be non empty set; func ComplexBoundedFunctionsNorm(X) -> Function of ComplexBoundedFunctions(X),REAL means :: CC0SP1:def 9 for x be object st x in ComplexBoundedFunctions(X) holds it.x = upper_bound PreNorms(modetrans(x,X)); end; theorem :: CC0SP1:12 for X being non empty set, f being Function of X,COMPLEX st f|X is bounded holds modetrans(f,X) = f; theorem :: CC0SP1:13 for X being non empty set, f being Function of X,COMPLEX st f|X is bounded holds (ComplexBoundedFunctionsNorm(X)).f = upper_bound PreNorms f; definition let X be non empty set; func C_Normed_Algebra_of_BoundedFunctions(X) -> Normed_Complex_AlgebraStr equals :: CC0SP1:def 10 Normed_Complex_AlgebraStr(# ComplexBoundedFunctions(X), mult_(ComplexBoundedFunctions(X),CAlgebra(X)), Add_(ComplexBoundedFunctions(X),CAlgebra(X)), Mult_(ComplexBoundedFunctions(X),CAlgebra(X)), One_(ComplexBoundedFunctions(X),CAlgebra(X)), Zero_(ComplexBoundedFunctions(X),CAlgebra(X)), ComplexBoundedFunctionsNorm(X) #); end; registration let X be non empty set; cluster C_Normed_Algebra_of_BoundedFunctions(X) -> non empty; end; registration let X be non empty set; cluster C_Normed_Algebra_of_BoundedFunctions(X) -> unital; end; theorem :: CC0SP1:14 for W being Normed_Complex_AlgebraStr, V being ComplexAlgebra st ComplexAlgebraStr(# the carrier of W,the multF of W, the addF of W,the Mult of W, the OneF of W,the ZeroF of W #) = V holds W is ComplexAlgebra; theorem :: CC0SP1:15 for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions(X) is ComplexAlgebra; theorem :: CC0SP1:16 for X being non empty set, F being Point of C_Normed_Algebra_of_BoundedFunctions(X) holds Mult_(ComplexBoundedFunctions(X),CAlgebra(X)).(1r,F) = F; theorem :: CC0SP1:17 for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions(X) is ComplexLinearSpace; theorem :: CC0SP1:18 for X being non empty set holds X --> 0 = 0.(C_Normed_Algebra_of_BoundedFunctions(X)); theorem :: CC0SP1:19 for X being non empty set, x being Element of X, f being Function of X,COMPLEX, F being Point of C_Normed_Algebra_of_BoundedFunctions(X) st f = F & f | X is bounded holds |.f.x.| <= ||.F.||; theorem :: CC0SP1:20 for X being non empty set, F being Point of C_Normed_Algebra_of_BoundedFunctions(X) holds 0 <= ||.F.||; theorem :: CC0SP1:21 for X being non empty set, F being Point of C_Normed_Algebra_of_BoundedFunctions(X) st F = 0.(C_Normed_Algebra_of_BoundedFunctions X) holds 0 = ||.F.||; theorem :: CC0SP1:22 for X being non empty set, f, g, h being Function of X,COMPLEX, F, G, H being Point of C_Normed_Algebra_of_BoundedFunctions(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 :: CC0SP1:23 for X being non empty set, a being Complex, f, g being Function of X,COMPLEX, F, G being Point of C_Normed_Algebra_of_BoundedFunctions(X) st f = F & g = G holds ( G = a*F iff for x being Element of X holds g.x = a*(f.x)); theorem :: CC0SP1:24 for X being non empty set, f, g, h being Function of X,COMPLEX, F, G, H being Point of C_Normed_Algebra_of_BoundedFunctions(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 :: CC0SP1:25 for X being non empty set, a being Complex, F, G being Point of C_Normed_Algebra_of_BoundedFunctions(X) holds ((||.F.|| = 0 implies F = 0.C_Normed_Algebra_of_BoundedFunctions(X)) & (F = 0.C_Normed_Algebra_of_BoundedFunctions(X) implies ||.F.|| = 0) & ||.(a*F).|| = (|.a.|)*||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.||); registration let X be non empty set; cluster C_Normed_Algebra_of_BoundedFunctions(X) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive ComplexNormSpace-like; end; theorem :: CC0SP1:26 for X being non empty set, f, g, h being Function of X,COMPLEX, F, G, H being Point of C_Normed_Algebra_of_BoundedFunctions(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 :: CC0SP1:27 for X being non empty set, seq being sequence of C_Normed_Algebra_of_BoundedFunctions(X) st seq is CCauchy holds seq is convergent; registration let X be non empty set; cluster C_Normed_Algebra_of_BoundedFunctions(X) -> complete; end; theorem :: CC0SP1:28 for X being non empty set holds C_Normed_Algebra_of_BoundedFunctions(X) is Complex_Banach_Algebra;