:: Banach Algebra of Continuous Functionals and Space of Real-valued Continuous Functionals with Bounded Support
:: by Katuhiko Kanazashi, Noboru Endou and Yasunari Shidama
::
:: Copyright (c) 2009-2021 Association of Mizar Users

definition
let X be 1-sorted ;
let y be Real;
func X --> y -> RealMap of X equals :: C0SP2:def 1
the carrier of X --> y;
coherence
the carrier of X --> y is RealMap of X
proof end;
end;

:: deftheorem defines --> C0SP2:def 1 :
for X being 1-sorted
for y being Real holds X --> y = the carrier of X --> y;

registration
let X be TopSpace;
let y be Real;
cluster X --> y -> continuous ;
coherence
X --> y is continuous
proof end;
end;

theorem Th1: :: C0SP2:1
for X being non empty TopSpace
for f being RealMap of X holds
( f is continuous iff for x being Point of X
for 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 ) )
proof end;

definition
let X be non empty TopSpace;
func ContinuousFunctions X -> Subset of (RAlgebra the carrier of X) equals :: C0SP2:def 2
{ f where f is continuous RealMap of X : verum } ;
correctness
coherence
{ f where f is continuous RealMap of X : verum } is Subset of (RAlgebra the carrier of X)
;
proof end;
end;

:: deftheorem defines ContinuousFunctions C0SP2:def 2 :
for X being non empty TopSpace holds ContinuousFunctions X = { f where f is continuous RealMap of X : verum } ;

registration
let X be non empty TopSpace;
coherence
not ContinuousFunctions X is empty
proof end;
end;

registration
let X be non empty TopSpace;
coherence
proof end;
end;

definition
let X be non empty TopSpace;
func R_Algebra_of_ContinuousFunctions X -> AlgebraStr equals :: C0SP2:def 3
AlgebraStr(# ,(mult_ (,(RAlgebra the carrier of X))),(Add_ (,(RAlgebra the carrier of X))),(Mult_ (,(RAlgebra the carrier of X))),(One_ (,(RAlgebra the carrier of X))),(Zero_ (,(RAlgebra the carrier of X))) #);
coherence
AlgebraStr(# ,(mult_ (,(RAlgebra the carrier of X))),(Add_ (,(RAlgebra the carrier of X))),(Mult_ (,(RAlgebra the carrier of X))),(One_ (,(RAlgebra the carrier of X))),(Zero_ (,(RAlgebra the carrier of X))) #) is AlgebraStr
;
end;

:: deftheorem defines R_Algebra_of_ContinuousFunctions C0SP2:def 3 :
for X being non empty TopSpace holds R_Algebra_of_ContinuousFunctions X = AlgebraStr(# ,(mult_ (,(RAlgebra the carrier of X))),(Add_ (,(RAlgebra the carrier of X))),(Mult_ (,(RAlgebra the carrier of X))),(One_ (,(RAlgebra the carrier of X))),(Zero_ (,(RAlgebra the carrier of X))) #);

theorem :: C0SP2:2
for X being non empty TopSpace holds R_Algebra_of_ContinuousFunctions X is Subalgebra of RAlgebra the carrier of X by C0SP1:6;

registration
let X be non empty TopSpace;
coherence ;
end;

registration
let X be non empty TopSpace;
coherence
proof end;
end;

theorem Th3: :: C0SP2:3
for X being non empty TopSpace
for F, G, H being VECTOR of
for f, g, h being RealMap of X 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) )
proof end;

theorem Th4: :: C0SP2:4
for X being non empty TopSpace
for F, G, H being VECTOR of
for f, g, h being RealMap of X
for a being Real st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
proof end;

theorem Th5: :: C0SP2:5
for X being non empty TopSpace
for F, G, H being VECTOR of
for f, g, h being RealMap of X 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) )
proof end;

theorem Th6: :: C0SP2:6
for X being non empty TopSpace holds 0. = X --> 0
proof end;

theorem Th7: :: C0SP2:7
for X being non empty TopSpace holds 1_ = X --> 1
proof end;

theorem Th8: :: C0SP2:8
for A being Algebra
for A1, A2 being Subalgebra of A st the carrier of A1 c= the carrier of A2 holds
A1 is Subalgebra of A2
proof end;

Lm1: for X being non empty compact TopSpace
for x being set st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X

proof end;

theorem :: C0SP2:9
for X being non empty compact TopSpace holds R_Algebra_of_ContinuousFunctions X is Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X
proof end;

definition
let X be non empty compact TopSpace;
func ContinuousFunctionsNorm X -> Function of ,REAL equals :: C0SP2:def 4
() | ;
correctness
coherence
() | is Function of ,REAL
;
proof end;
end;

:: deftheorem defines ContinuousFunctionsNorm C0SP2:def 4 :
for X being non empty compact TopSpace holds ContinuousFunctionsNorm X = () | ;

definition
let X be non empty compact TopSpace;
func R_Normed_Algebra_of_ContinuousFunctions X -> Normed_AlgebraStr equals :: C0SP2:def 5
Normed_AlgebraStr(# ,(mult_ (,(RAlgebra the carrier of X))),(Add_ (,(RAlgebra the carrier of X))),(Mult_ (,(RAlgebra the carrier of X))),(One_ (,(RAlgebra the carrier of X))),(Zero_ (,(RAlgebra the carrier of X))), #);
correctness
coherence
Normed_AlgebraStr(# ,(mult_ (,(RAlgebra the carrier of X))),(Add_ (,(RAlgebra the carrier of X))),(Mult_ (,(RAlgebra the carrier of X))),(One_ (,(RAlgebra the carrier of X))),(Zero_ (,(RAlgebra the carrier of X))), #) is Normed_AlgebraStr
;
;
end;

:: deftheorem defines R_Normed_Algebra_of_ContinuousFunctions C0SP2:def 5 :
for X being non empty compact TopSpace holds R_Normed_Algebra_of_ContinuousFunctions X = Normed_AlgebraStr(# ,(mult_ (,(RAlgebra the carrier of X))),(Add_ (,(RAlgebra the carrier of X))),(Mult_ (,(RAlgebra the carrier of X))),(One_ (,(RAlgebra the carrier of X))),(Zero_ (,(RAlgebra the carrier of X))), #);

registration
let X be non empty compact TopSpace;
correctness
coherence ;
;
end;

Lm2: now :: thesis: for X being non empty compact TopSpace
for x, e being Element of st e = One_ (,(RAlgebra the carrier of X)) holds
( x * e = x & e * x = x )
let X be non empty compact TopSpace; :: thesis: for x, e being Element of st e = One_ (,(RAlgebra the carrier of X)) holds
( x * e = x & e * x = x )

set F = R_Normed_Algebra_of_ContinuousFunctions X;
let x, e be Element of ; :: thesis: ( e = One_ (,(RAlgebra the carrier of X)) implies ( x * e = x & e * x = x ) )
assume A1: e = One_ (,(RAlgebra the carrier of X)) ; :: thesis: ( x * e = x & e * x = x )
set X1 = ContinuousFunctions X;
reconsider f = x as Element of ContinuousFunctions X ;
1_ (RAlgebra the carrier of X) = X --> 1
.= 1_ by Th7 ;
then A2: ( [f,(1_ (RAlgebra the carrier of X))] in & [(1_ (RAlgebra the carrier of X)),f] in ) by ZFMISC_1:87;
x * e = (mult_ (,(RAlgebra the carrier of X))) . (f,(1_ (RAlgebra the carrier of X))) by ;
then x * e = ( the multF of (RAlgebra the carrier of X) || ) . (f,(1_ (RAlgebra the carrier of X))) by C0SP1:def 6;
then x * e = f * (1_ (RAlgebra the carrier of X)) by ;
hence x * e = x ; :: thesis: e * x = x
e * x = (mult_ (,(RAlgebra the carrier of X))) . ((1_ (RAlgebra the carrier of X)),f) by ;
then e * x = ( the multF of (RAlgebra the carrier of X) || ) . ((1_ (RAlgebra the carrier of X)),f) by C0SP1:def 6;
then e * x = (1_ (RAlgebra the carrier of X)) * f by ;
hence e * x = x ; :: thesis: verum
end;

registration
let X be non empty compact TopSpace;
correctness
proof end;
end;

theorem Th10: :: C0SP2:10
for W being Normed_AlgebraStr
for V being Algebra st AlgebraStr(# 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 Algebra
proof end;

Lm3: for X being non empty compact TopSpace
for x being Point of
for y being Point of () st x = y holds
=

by FUNCT_1:49;

Lm4: for X being non empty compact TopSpace
for x1, x2 being Point of
for y1, y2 being Point of () st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2

proof end;

Lm5: for X being non empty compact TopSpace
for a being Real
for x being Point of
for y being Point of () st x = y holds
a * x = a * y

proof end;

Lm6: for X being non empty compact TopSpace
for x1, x2 being Point of
for y1, y2 being Point of () st x1 = y1 & x2 = y2 holds
x1 * x2 = y1 * y2

proof end;

registration end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem Th11: :: C0SP2:11
for X being non empty compact TopSpace
for F being Point of holds (Mult_ (,(RAlgebra the carrier of X))) . (1,F) = F
proof end;

registration end;

theorem Th12: :: C0SP2:12
for X being non empty compact TopSpace holds X --> 0 = 0.
proof end;

Lm7: for X being non empty compact TopSpace holds 0. = 0. ()
proof end;

Lm8: for X being non empty compact TopSpace holds 1. = 1. ()
proof end;

theorem :: C0SP2:13
for X being non empty compact TopSpace
for F being Point of holds 0 <=
proof end;

theorem :: C0SP2:14
for X being non empty compact TopSpace
for F being Point of st F = 0. holds
0 =
proof end;

theorem Th15: :: C0SP2:15
for X being non empty compact TopSpace
for F, G, H being Point of
for f, g, h being RealMap of 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) )
proof end;

theorem :: C0SP2:16
for a being Real
for X being non empty compact TopSpace
for F, G being Point of
for f, g being RealMap of X st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
proof end;

theorem :: C0SP2:17
for X being non empty compact TopSpace
for F, G, H being Point of
for f, g, h being RealMap of 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) )
proof end;

theorem Th18: :: C0SP2:18
for a being Real
for X being non empty compact TopSpace
for F, G being Point of holds
( ( = 0 implies F = 0. ) & ( F = 0. implies = 0 ) & ||.(a * F).|| = |.a.| * & ||.(F + G).|| <= + )
proof end;

registration
let X be non empty compact TopSpace;
coherence
proof end;
end;

Lm9: for X being non empty compact TopSpace
for x1, x2 being Point of
for y1, y2 being Point of () st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2

proof end;

theorem :: C0SP2:19
for X being non empty compact TopSpace
for F, G, H being Point of
for f, g, h being RealMap of 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) )
proof end;

theorem Th20: :: C0SP2:20
for X being RealBanachSpace
for Y being Subset of X
for seq being 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 ) by ;

theorem Th21: :: C0SP2:21
for X being non empty compact TopSpace
for Y being Subset of () st Y = ContinuousFunctions X holds
Y is closed
proof end;

theorem Th22: :: C0SP2:22
for X being non empty compact TopSpace
for seq being sequence of st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof end;

registration
let X be non empty compact TopSpace;
coherence
proof end;
end;

registration end;

theorem Th23: :: C0SP2:23
for X being non empty TopSpace
for f, g being RealMap of X holds support (f + g) c= () \/ ()
proof end;

theorem Th24: :: C0SP2:24
for X being non empty TopSpace
for a being Real
for f being RealMap of X holds support (a (#) f) c= support f
proof end;

theorem :: C0SP2:25
for X being non empty TopSpace
for f, g being RealMap of X holds support (f (#) g) c= () \/ ()
proof end;

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 being 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 ) ) )
}
;
correctness
coherence
{ f where f is RealMap of X : ( f is continuous & ex Y being 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 ) ) )
}
is non empty Subset of (RealVectSpace the carrier of X)
;
proof end;
end;

:: deftheorem defines C_0_Functions C0SP2:def 6 :
for X being non empty TopSpace holds C_0_Functions X = { f where f is RealMap of X : ( f is continuous & ex Y being 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 ) ) )
}
;

theorem :: C0SP2:26
for X being non empty TopSpace holds C_0_Functions X is non empty Subset of (RAlgebra the carrier of X) ;

Lm10: for X being non empty TopSpace
for v, u being Element of (RAlgebra the carrier of X) st v in C_0_Functions X & u in C_0_Functions X holds
v + u in C_0_Functions X

proof end;

Lm11: for X being non empty TopSpace
for a being Real
for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
a * u in C_0_Functions X

proof end;

Lm12: for X being non empty TopSpace
for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds
- u in C_0_Functions X

proof end;

theorem :: C0SP2:27
for X being non empty TopSpace
for W being non empty Subset of (RAlgebra the carrier of X) st W = C_0_Functions X holds
proof end;

theorem Th28: :: C0SP2:28
for X being non empty TopSpace holds C_0_Functions X is linearly-closed
proof end;

registration
let X be non empty TopSpace;
correctness
coherence
( not C_0_Functions X is empty & C_0_Functions X is linearly-closed )
;
by Th28;
end;

definition
let X be non empty TopSpace;
func R_VectorSpace_of_C_0_Functions X -> RealLinearSpace equals :: C0SP2:def 7
RLSStruct(# (),(Zero_ ((),(RealVectSpace the carrier of X))),(Add_ ((),(RealVectSpace the carrier of X))),(Mult_ ((),(RealVectSpace the carrier of X))) #);
correctness
coherence
RLSStruct(# (),(Zero_ ((),(RealVectSpace the carrier of X))),(Add_ ((),(RealVectSpace the carrier of X))),(Mult_ ((),(RealVectSpace the carrier of X))) #) is RealLinearSpace
;
end;

:: deftheorem defines R_VectorSpace_of_C_0_Functions C0SP2:def 7 :
for X being non empty TopSpace holds R_VectorSpace_of_C_0_Functions X = RLSStruct(# (),(Zero_ ((),(RealVectSpace the carrier of X))),(Add_ ((),(RealVectSpace the carrier of X))),(Mult_ ((),(RealVectSpace the carrier of X))) #);

theorem :: C0SP2:29
for X being non empty TopSpace holds R_VectorSpace_of_C_0_Functions X is Subspace of RealVectSpace the carrier of X by RSSPACE:11;

theorem Th30: :: C0SP2:30
for X being non empty TopSpace
for x being set st x in C_0_Functions X holds
x in BoundedFunctions the carrier of X
proof end;

definition
let X be non empty TopSpace;
func C_0_FunctionsNorm X -> Function of (),REAL equals :: C0SP2:def 8
() | ();
correctness
coherence
() | () is Function of (),REAL
;
proof end;
end;

:: deftheorem defines C_0_FunctionsNorm C0SP2:def 8 :
for X being non empty TopSpace holds C_0_FunctionsNorm X = () | ();

definition
let X be non empty TopSpace;
func R_Normed_Space_of_C_0_Functions X -> non empty NORMSTR equals :: C0SP2:def 9
NORMSTR(# (),(Zero_ ((),(RealVectSpace the carrier of X))),(Add_ ((),(RealVectSpace the carrier of X))),(Mult_ ((),(RealVectSpace the carrier of X))), #);
correctness
coherence
NORMSTR(# (),(Zero_ ((),(RealVectSpace the carrier of X))),(Add_ ((),(RealVectSpace the carrier of X))),(Mult_ ((),(RealVectSpace the carrier of X))), #) is non empty NORMSTR
;
;
end;

:: deftheorem defines R_Normed_Space_of_C_0_Functions C0SP2:def 9 :
for X being non empty TopSpace holds R_Normed_Space_of_C_0_Functions X = NORMSTR(# (),(Zero_ ((),(RealVectSpace the carrier of X))),(Add_ ((),(RealVectSpace the carrier of X))),(Mult_ ((),(RealVectSpace the carrier of X))), #);

registration
let X be non empty TopSpace;
correctness
coherence ;
;
end;

theorem :: C0SP2:31
for X being non empty TopSpace
for x being set st x in C_0_Functions X holds
x in ContinuousFunctions X
proof end;

theorem Th32: :: C0SP2:32
for X being non empty TopSpace holds 0. = X --> 0
proof end;

theorem Th33: :: C0SP2:33
for X being non empty TopSpace holds 0. = X --> 0
proof end;

Lm13: for X being non empty TopSpace
for x1, x2 being Point of
for y1, y2 being Point of () st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2

proof end;

Lm14: for X being non empty TopSpace
for a being Real
for x being Point of
for y being Point of () st x = y holds
a * x = a * y

proof end;

theorem Th34: :: C0SP2:34
for a being Real
for X being non empty TopSpace
for F, G being Point of holds
( ( = 0 implies F = 0. ) & ( F = 0. implies = 0 ) & ||.(a * F).|| = |.a.| * & ||.(F + G).|| <= + )
proof end;

theorem Th35: :: C0SP2:35
for X being non empty TopSpace holds R_Normed_Space_of_C_0_Functions X is RealNormSpace-like
proof end;

registration
let X be non empty TopSpace;
coherence
proof end;
end;

theorem :: C0SP2:36
for X being non empty TopSpace holds R_Normed_Space_of_C_0_Functions X is RealNormSpace ;