:: 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-2016 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;