:: Banach Algebra of Continuous Functionals and Space of Real-valued
:: Continuous Functionals with Bounded Support
:: by Katuhiko Kanazashi, Noboru Endou and Yasunari Shidama
::
:: Received October 20, 2009
:: Copyright (c) 2009-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, PSCOMP_1, NUMBERS, PRE_TOPC, ORDINAL2,
SUBSET_1, RCOMP_1, RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1, ARYTM_3,
XXREAL_1, ARYTM_1, COMPLEX1, CONNSP_2, RLVECT_1, ALGSTR_0, FUNCSDOM,
REAL_1, FUNCT_2, C0SP1, IDEAL_1, VALUED_1, MESFUNC1, RSSPACE, POLYALG1,
BINOP_1, VECTSP_1, SUPINF_2, GROUP_1, REALSET1, ZFMISC_1, RSSPACE4,
XXREAL_2, XXREAL_0, LOPBAN_2, NORMSP_1, REWRITE1, NAT_1, RSSPACE3, SEQ_2,
PARTFUN1, SEQFUNC, C0SP2, LOPBAN_1, METRIC_1, RELAT_2, PRE_POLY, RLSUB_1,
TOPMETR, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, REALSET1, FUNCT_1,
FUNCT_2, STRUCT_0, ALGSTR_0, IDEAL_1, BINOP_1, DOMAIN_1, RELSET_1,
PRE_TOPC, COMPTS_1, PSCOMP_1, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM,
PARTFUN1, SEQFUNC, RSSPACE3, RCOMP_1, SEQ_2, NORMSP_0, NORMSP_1,
NFCONT_1, LOPBAN_1, LOPBAN_2, C0SP1, CONNSP_2, FUNCOP_1, PRE_POLY,
XXREAL_2, VALUED_1, RLSUB_1, RSSPACE, TOPMETR;
constructors REAL_1, REALSET1, RSSPACE3, COMPLEX1, RCOMP_1, IDEAL_1, C0SP1,
NFCONT_1, SEQFUNC, MEASURE6, PRE_POLY, TOPMETR, RLSUB_1, SEQ_4, NAGATA_1,
PSCOMP_1, COMPTS_1, COMSEQ_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, REALSET1,
ALGSTR_0, NUMBERS, ORDINAL1, MEMBERED, FUNCSDOM, VECTSP_1, VECTSP_2,
VALUED_0, LOPBAN_2, PSCOMP_1, RCOMP_1, C0SP1, COMPTS_1, XXREAL_0,
FUNCT_2, VALUED_1, XXREAL_2, TOPMETR, RELSET_1, WAYBEL_2, JORDAN5A;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin :: Banach Algebra of Continuous Functionals
definition
let X be 1-sorted, y be Real;
func X --> y -> RealMap of X equals
:: C0SP2:def 1
(the carrier of X) --> y;
end;
registration
let X be TopSpace, y be Real;
cluster X --> y -> continuous;
end;
theorem :: C0SP2:1
for X being non empty TopSpace, f be RealMap of X holds f is continuous iff
for x being Point of X,V being Subset of REAL 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;
definition let X be non empty TopSpace;
func ContinuousFunctions(X) -> Subset of RAlgebra the carrier of X equals
:: C0SP2:def 2
the set of all f where f is continuous RealMap of X ;
end;
registration
let X be non empty TopSpace;
cluster ContinuousFunctions(X) -> non empty;
end;
registration
let X be non empty TopSpace;
cluster ContinuousFunctions(X) -> additively-linearly-closed
multiplicatively-closed;
end;
definition
let X be non empty TopSpace;
func R_Algebra_of_ContinuousFunctions(X) -> AlgebraStr equals
:: C0SP2:def 3
AlgebraStr (# ContinuousFunctions(X),
mult_(ContinuousFunctions(X),RAlgebra the carrier of X),
Add_(ContinuousFunctions(X),RAlgebra the carrier of X),
Mult_(ContinuousFunctions(X),RAlgebra the carrier of X),
One_(ContinuousFunctions(X),RAlgebra the carrier of X),
Zero_(ContinuousFunctions(X),RAlgebra the carrier of X) #);
end;
theorem :: C0SP2:2
for X being non empty TopSpace holds
R_Algebra_of_ContinuousFunctions(X)
is Subalgebra of RAlgebra the carrier of X;
registration
let X be non empty TopSpace;
cluster R_Algebra_of_ContinuousFunctions(X) -> strict non empty;
end;
registration
let X be non empty TopSpace;
cluster R_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 :: C0SP2:3
for X being non empty TopSpace
for F,G,H being VECTOR of R_Algebra_of_ContinuousFunctions(X)
for f,g,h being RealMap of X holds
(f=F & g=G & h=H implies ( H = F+G iff (for x be Element of the carrier of X
holds h.x = f.x + g.x)));
theorem :: C0SP2:4
for X being non empty TopSpace
for F,G,H being VECTOR of R_Algebra_of_ContinuousFunctions(X)
for f,g,h being RealMap of X
for a being Real
holds
(f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x ));
theorem :: C0SP2:5
for X being non empty TopSpace
for F,G,H being VECTOR of R_Algebra_of_ContinuousFunctions(X)
for f,g,h being RealMap of X holds
(f=F & g=G & h=H implies ( H = F*G iff (for x be Element of the carrier of X
holds h.x = f.x * g.x)));
theorem :: C0SP2:6
for X being non empty TopSpace holds
0.R_Algebra_of_ContinuousFunctions(X) = X --> 0;
theorem :: C0SP2:7
for X being non empty TopSpace holds
1_R_Algebra_of_ContinuousFunctions(X) = X --> 1;
theorem :: C0SP2:8
for A being Algebra, A1,A2 being Subalgebra of A holds
the carrier of A1 c= the carrier of A2 implies A1 is Subalgebra of A2;
theorem :: C0SP2:9
for X being compact non empty TopSpace holds
(R_Algebra_of_ContinuousFunctions(X) is
Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X);
definition
let X be compact non empty TopSpace;
func ContinuousFunctionsNorm(X) -> Function of (ContinuousFunctions(X)),REAL
equals
:: C0SP2:def 4
(BoundedFunctionsNorm the carrier of X)|(ContinuousFunctions(X));
end;
definition
let X be compact non empty TopSpace;
func R_Normed_Algebra_of_ContinuousFunctions(X) -> Normed_AlgebraStr equals
:: C0SP2:def 5
Normed_AlgebraStr (# ContinuousFunctions(X),
mult_(ContinuousFunctions(X),RAlgebra the carrier of X),
Add_(ContinuousFunctions(X),RAlgebra the carrier of X),
Mult_(ContinuousFunctions(X),RAlgebra the carrier of X),
One_(ContinuousFunctions(X),RAlgebra the carrier of X),
Zero_(ContinuousFunctions(X),RAlgebra the carrier of X),
ContinuousFunctionsNorm(X) #);
end;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> strict non empty;
end;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> unital;
end;
theorem :: C0SP2:10
for W be Normed_AlgebraStr, V be Algebra st
the AlgebraStr of W = V holds W is Algebra;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) ->
Abelian add-associative right_zeroed right_complementable
commutative associative right_unital right-distributive
vector-distributive scalar-distributive scalar-associative
vector-associative;
end;
theorem :: C0SP2:11
for X being compact non empty TopSpace
for F being Point of R_Normed_Algebra_of_ContinuousFunctions(X) holds
(Mult_(ContinuousFunctions(X), RAlgebra the carrier of X)).(1,F) = F;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> vector-distributive
scalar-distributive scalar-associative scalar-unital;
end;
theorem :: C0SP2:12
for X being compact non empty TopSpace holds
X --> 0 = 0.R_Normed_Algebra_of_ContinuousFunctions(X);
theorem :: C0SP2:13
for X be compact non empty TopSpace
for F be Point of R_Normed_Algebra_of_ContinuousFunctions(X)
holds 0 <= ||.F.||;
theorem :: C0SP2:14
for X being compact non empty TopSpace
for F be Point of R_Normed_Algebra_of_ContinuousFunctions(X) holds
F = 0.R_Normed_Algebra_of_ContinuousFunctions(X) implies 0 = ||.F.||;
theorem :: C0SP2:15
for X being compact non empty TopSpace
for F,G,H being Point of R_Normed_Algebra_of_ContinuousFunctions(X)
for f,g,h be RealMap of X
holds
(f=F & g=G & h=H implies
(H = F+G iff for x be Element of X holds h.x = f.x + g.x));
theorem :: C0SP2:16
for a be Real
for X being compact non empty TopSpace
for F,G being Point of R_Normed_Algebra_of_ContinuousFunctions(X)
for f,g being RealMap of X holds
(f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x ));
theorem :: C0SP2:17
for X being compact non empty TopSpace
for F,G,H being Point of R_Normed_Algebra_of_ContinuousFunctions(X)
for f,g,h being RealMap of X holds
(f=F & g=G & h=H implies
(H = F*G iff for x be Element of X holds h.x = f.x * g.x));
theorem :: C0SP2:18
for a being Real
for X being compact non empty TopSpace
for F,G being Point of R_Normed_Algebra_of_ContinuousFunctions(X) holds
( ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_ContinuousFunctions(X)) &
(||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||);
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) ->
reflexive discerning RealNormSpace-like;
end;
theorem :: C0SP2:19
for X be compact non empty TopSpace
for F,G,H be Point of R_Normed_Algebra_of_ContinuousFunctions(X)
for f,g,h be RealMap of X holds
f=F & g=G & h=H implies
(H = F-G iff (for x be Element of X holds h.x = f.x - g.x));
theorem :: C0SP2:20
for X be RealBanachSpace, Y be Subset of X, seq be sequence of X st
Y is closed & rng seq c= Y & seq is Cauchy_sequence_by_Norm holds
seq is convergent & lim seq in Y;
theorem :: C0SP2:21
for X be compact non empty TopSpace
for Y be Subset of R_Normed_Algebra_of_BoundedFunctions the carrier of X st
Y = ContinuousFunctions(X) holds Y is closed;
theorem :: C0SP2:22
for X be compact non empty TopSpace
for seq be sequence of R_Normed_Algebra_of_ContinuousFunctions(X) st
seq is Cauchy_sequence_by_Norm holds seq is convergent;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> complete;
end;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> Banach_Algebra-like;
end;
begin :: Some properties of support
theorem :: C0SP2:23
for X be non empty TopSpace
for f,g be RealMap of X holds
support(f+g) c= support(f) \/ support(g);
theorem :: C0SP2:24
for X be non empty TopSpace
for a be Real,f be RealMap of X holds
support(a(#)f) c= support(f);
theorem :: C0SP2:25
for X be non empty TopSpace
for f,g be RealMap of X holds support(f(#)g) c= support(f) \/ support(g);
begin :: Space of Real-valued Continuous Functionals with Bounded Support
definition
let X be non empty TopSpace;
func C_0_Functions(X) -> non empty Subset of RealVectSpace the carrier of X
equals
:: C0SP2:def 6
{ f where f is RealMap of X : 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 :: C0SP2:26
for X be non empty TopSpace holds
C_0_Functions(X) is non empty Subset of RAlgebra the carrier of X;
theorem :: C0SP2:27
for X be non empty TopSpace
for W be non empty Subset of RAlgebra the carrier of X
st W = C_0_Functions(X) holds W is additively-linearly-closed;
theorem :: C0SP2:28
for X be non empty TopSpace holds
C_0_Functions(X) is linearly-closed;
registration
let X be non empty TopSpace;
cluster C_0_Functions(X) -> non empty linearly-closed;
end;
definition
let X be non empty TopSpace;
func R_VectorSpace_of_C_0_Functions(X) -> RealLinearSpace equals
:: C0SP2:def 7
RLSStruct (# C_0_Functions(X),
Zero_(C_0_Functions(X), RealVectSpace(the carrier of X)),
Add_(C_0_Functions(X), RealVectSpace(the carrier of X)),
Mult_(C_0_Functions(X), RealVectSpace(the carrier of X)) #);
end;
theorem :: C0SP2:29
for X be non empty TopSpace holds
R_VectorSpace_of_C_0_Functions(X)
is Subspace of RealVectSpace(the carrier of X);
theorem :: C0SP2:30
for X be non empty TopSpace
for x being set st x in C_0_Functions(X) holds
x in BoundedFunctions the carrier of X;
definition
let X be non empty TopSpace;
func C_0_FunctionsNorm X -> Function of (C_0_Functions(X)),REAL equals
:: C0SP2:def 8
(BoundedFunctionsNorm the carrier of X)|(C_0_Functions(X));
end;
definition
let X be non empty TopSpace;
func R_Normed_Space_of_C_0_Functions(X) -> non empty NORMSTR equals
:: C0SP2:def 9
NORMSTR (# C_0_Functions(X),
Zero_(C_0_Functions(X), RealVectSpace(the carrier of X)),
Add_(C_0_Functions(X), RealVectSpace(the carrier of X)),
Mult_(C_0_Functions(X), RealVectSpace(the carrier of X)),
C_0_FunctionsNorm X #);
end;
registration
let X be non empty TopSpace;
cluster R_Normed_Space_of_C_0_Functions(X) -> strict non empty;
end;
theorem :: C0SP2:31
for X be non empty TopSpace
for x being set st x in C_0_Functions(X) holds
x in ContinuousFunctions(X);
theorem :: C0SP2:32
for X be non empty TopSpace holds
0.R_VectorSpace_of_C_0_Functions(X) = X -->0;
theorem :: C0SP2:33
for X be non empty TopSpace holds
0.R_Normed_Space_of_C_0_Functions(X) = X --> 0;
theorem :: C0SP2:34
for a be Real
for X be non empty TopSpace
for F,G be Point of R_Normed_Space_of_C_0_Functions(X) holds
(||.F.|| = 0 iff F = 0.R_Normed_Space_of_C_0_Functions(X) ) &
||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||;
theorem :: C0SP2:35
for X be non empty TopSpace holds
R_Normed_Space_of_C_0_Functions(X) is RealNormSpace-like;
registration
let X be non empty TopSpace;
cluster R_Normed_Space_of_C_0_Functions(X) ->
reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
end;
theorem :: C0SP2:36
for X be non empty TopSpace holds
R_Normed_Space_of_C_0_Functions(X) is RealNormSpace;