:: Banach Algebra of Continuous Functionals
:: by Kanazashi Katuhiko , Noboru Endou and Yasunari Shidama
::
:: Received October 20, 2009
:: Copyright (c) 2009 Association of Mizar Users
environ
vocabularies STRUCT_0, XREAL_0, ORDINAL1, 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;
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, PARTFUN3;
constructors REAL_1, REALSET1, RSSPACE3, COMPLEX1, RCOMP_1, IDEAL_1, COMPTS_1,
SEQ_1, C0SP1, NFCONT_1, SEQFUNC, JORDAN_A, PARTFUN3, BINOP_2, SEQ_2,
MEASURE6;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, REALSET1,
ALGSTR_0, NUMBERS, ORDINAL1, MEMBERED, FUNCSDOM, RELAT_1, VECTSP_1,
VECTSP_2, VALUED_0, LOPBAN_2, PSCOMP_1, RCOMP_1, C0SP1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions PSCOMP_1, REALSET1, ALGSTR_0, TARSKI, XCMPLX_0, NORMSP_1, RCOMP_1,
FUNCSDOM, RLVECT_1, VECTSP_1, STRUCT_0, GROUP_1, BINOP_1, C0SP1,
NORMSP_0;
theorems RFUNCT_1, FUNCT_1, NFCONT_1, PARTFUN1, SEQ_2, ABSVALUE, ALGSTR_0,
COMPLEX1, ZFMISC_1, TARSKI, RCOMP_1, XBOOLE_1, PSCOMP_1, IDEAL_1,
RSSPACE3, RELAT_1, XREAL_0, XXREAL_0, FUNCSDOM, NORMSP_1, LOPBAN_1,
FUNCT_2, XREAL_1, RLVECT_1, TOPS_1, FUNCOP_1, VECTSP_1, GROUP_1,
LOPBAN_2, VALUED_1, C0SP1, CONNSP_2, XXREAL_1, NORMSP_0;
begin
definition
let X be 1-sorted, y be real number;
func X --> y -> RealMap of X equals
(the carrier of X) --> y;
coherence
proof
y in REAL by XREAL_0:def 1; then
(the carrier of X) --> y is RealMap of X by FUNCOP_1:57;
hence thesis;
end;
end;
registration
let X be TopSpace, y be real number;
cluster X --> y -> continuous;
coherence
proof
set f = X --> y;
set HX=[#] X;
let P1 being Subset of REAL such that P1 is closed;
per cases;
suppose y in P1;
then f"P1 = HX by FUNCOP_1:20;
hence f"P1 is closed;
end;
suppose not y in P1;
then f"P1 = {}X by FUNCOP_1:22;
hence f"P1 is closed;
end;
end;
end;
theorem Th1:
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
proof
let X be non empty TopSpace,f be RealMap of X;
hereby assume A1: f is continuous;
now let x be Point of X,V being Subset of REAL;
set r = f.x;
assume r in V & V is open; then
consider r0 be real number such that
A2: 0 Subset of RAlgebra the carrier of X equals
{ f where f is continuous RealMap of X : not contradiction };
correctness
proof
set A = { f where f is continuous RealMap of X : not contradiction };
A c= Funcs(the carrier of X,REAL)
proof
let x be set;
assume x in A;
then ex f be continuous RealMap of X st x=f;
hence x in Funcs(the carrier of X,REAL) by FUNCT_2:11;
end;
hence thesis;
end;
end;
registration let X;
cluster ContinuousFunctions(X) -> non empty;
coherence
proof
X-->0 in { f where f is continuous RealMap of X : not contradiction };
hence thesis;
end;
end;
registration let X;
cluster ContinuousFunctions X -> additively-linearly-closed
multiplicatively-closed;
coherence
proof
set W = ContinuousFunctions X;
set V = RAlgebra the carrier of X;
A1:RAlgebra the carrier of X is RealLinearSpace by C0SP1:7;
for v,u be Element of V st v in W & u in W holds v + u in W
proof
let v,u be Element of V such that
A2: v in W & u in W;
consider v1 be continuous RealMap of X such that
A3:v1=v by A2;
consider u1 be continuous RealMap of X such that
A4:u1=u by A2;
reconsider h = v+u as Element of Funcs(the carrier of X,REAL);
A5:ex f being Function st
h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
dom v1 /\ dom u1 = (the carrier of X) /\ dom u1 by FUNCT_2:def 1; then
A6: dom v1 /\ dom u1 = (the carrier of X) /\ (the carrier of X)
by FUNCT_2:def 1;
for x be set st x in dom h holds h.x = v1.x + u1.x
by A3,A4,FUNCSDOM:10; then
v+u=v1+u1 by A6,A5,VALUED_1:def 1;
hence v+u in W;
end; then
A7:W is add-closed by IDEAL_1:def 1;
for v be Element of V st v in W holds -v in W
proof
let v be Element of V such that
A8: v in W;
consider v1 be continuous RealMap of X such that
A9:v1=v by A8;
reconsider h = -v, v2 = v as Element of Funcs(the carrier of X,REAL);
A10: h=(-1)*v by A1,RLVECT_1:29;
A11:ex f being Function st
h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
A12: dom v1 =the carrier of X by FUNCT_2:def 1;
now let x be set;
assume x in dom h; then
reconsider y=x as Element of the carrier of X;
h.x = (-1)*(v2.y) by A10,FUNCSDOM:15;
hence h.x = -v1.x by A9;
end; then
-v=-v1 by A12,A11,VALUED_1:9;
hence -v in W;
end; then
A13:W is having-inverse by C0SP1:def 1;
for a be Real, u be Element of V st u in W holds a * u in W
proof
let a be Real, u be Element of V such that
A14: u in W;
consider u1 be continuous RealMap of X such that
A15:u1=u by A14;
reconsider h = a*u as Element of Funcs(the carrier of X,REAL);
A16:ex f being Function st
h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
A17: dom u1 = the carrier of X by FUNCT_2:def 1;
for x be set st x in dom h holds h.x = a*(u1.x) by A15,FUNCSDOM:15; then
a*u=a(#)u1 by A17,A16,VALUED_1:def 5;
hence a*u in W;
end;
hence ContinuousFunctions X is additively-linearly-closed
by A7,A13,C0SP1:def 10;
A18:for v,u be Element of V st v in W & u in W holds v * u in W
proof
let v,u be Element of V such that
A19: v in W & u in W;
consider v1 be continuous RealMap of X such that
A20:v1=v by A19;
consider u1 be continuous RealMap of X such that
A21:u1=u by A19;
reconsider h = v*u as Element of Funcs(the carrier of X,REAL);
A22:ex f being Function st
h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
dom v1 /\ dom u1 = (the carrier of X) /\ dom u1 by FUNCT_2:def 1; then
A23: dom v1 /\ dom u1 = (the carrier of X) /\ (the carrier of X)
by FUNCT_2:def 1;
for x be set st x in dom h holds h.x = v1.x *u1.x
by A20,A21,FUNCSDOM:11; then
v*u=v1(#)u1 by A23,A22,VALUED_1:def 4;
hence v*u in W;
end;
reconsider g = RealFuncUnit the carrier of X as RealMap of X;
g = X --> 1; then
1.V in W;
hence thesis by A18,C0SP1:def 4;
end;
end;
definition let X be non empty TopSpace;
func R_Algebra_of_ContinuousFunctions X -> AlgebraStr equals
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)
#);
coherence;
end;
theorem
R_Algebra_of_ContinuousFunctions X
is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
registration let X;
cluster R_Algebra_of_ContinuousFunctions X -> strict non empty;
coherence;
end;
registration let X;
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;
coherence
proof
A1: R_Algebra_of_ContinuousFunctions X is Algebra by C0SP1:6;
now let v be VECTOR of R_Algebra_of_ContinuousFunctions X;
reconsider v1=v as VECTOR of RAlgebra the carrier of X by TARSKI:def 3;
R_Algebra_of_ContinuousFunctions X
is Subalgebra of RAlgebra the carrier of X by C0SP1:6; then
1 * v = 1*v1 by C0SP1:8;
hence 1 * v =v by FUNCSDOM:23;
end;
hence thesis by A1,RLVECT_1:def 11;
end;
end;
reserve F,G,H for VECTOR of R_Algebra_of_ContinuousFunctions X;
reserve f,g,h for RealMap of X;
reserve a for Real;
theorem Th3:
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) )
proof
assume A1: f=F & g=G & h=H;
A2:R_Algebra_of_ContinuousFunctions X is
Subalgebra of RAlgebra the carrier of X by C0SP1:6;
reconsider f1=F, g1=G, h1=H as VECTOR of
RAlgebra the carrier of X by TARSKI:def 3;
hereby assume A3: H = F+G;
let x be Element of the carrier of X;
h1=f1+g1 by A2,A3,C0SP1:8;
hence h.x = f.x+g.x by A1,FUNCSDOM:10;
end;
assume for x be Element of X holds h.x = f.x+g.x; then
h1=f1+g1 by A1,FUNCSDOM:10;
hence H =F+G by A2,C0SP1:8;
end;
theorem Th4:
f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x )
proof
assume A1: f=F & g=G;
A2:R_Algebra_of_ContinuousFunctions X is
Subalgebra of RAlgebra the carrier of X by C0SP1:6;
reconsider f1=F, g1=G as VECTOR of
RAlgebra the carrier of X by TARSKI:def 3;
hereby assume A3: G = a*F;
let x be Element of the carrier of X;
g1=a*f1 by A2,A3,C0SP1:8;
hence g.x=a*f.x by A1,FUNCSDOM:15;
end;
assume for x be Element of the carrier of X holds g.x=a*f.x; then
g1=a*f1 by A1,FUNCSDOM:15;
hence G =a*F by A2,C0SP1:8;
end;
theorem Th5:
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) )
proof
assume A1: f=F & g=G & h=H;
A2:R_Algebra_of_ContinuousFunctions X is
Subalgebra of RAlgebra the carrier of X by C0SP1:6;
reconsider f1=F, g1=G, h1=H as VECTOR of
RAlgebra the carrier of X by TARSKI:def 3;
hereby assume A3: H = F*G;
let x be Element of the carrier of X;
h1 = f1*g1 by A2,A3,C0SP1:8;
hence h.x = f.x * g.x by A1,FUNCSDOM:11;
end;
assume for x be Element of X holds h.x = f.x * g.x; then
h1 = f1 * g1 by A1,FUNCSDOM:11;
hence H = F * G by A2,C0SP1:8;
end;
theorem Th6:
0.R_Algebra_of_ContinuousFunctions X = X --> 0
proof
A1:R_Algebra_of_ContinuousFunctions X
is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
0.RAlgebra the carrier of X = X --> 0;
hence thesis by A1,C0SP1:8;
end;
theorem Th7:
1_R_Algebra_of_ContinuousFunctions X = X --> 1
proof
A1:R_Algebra_of_ContinuousFunctions X
is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
1_RAlgebra the carrier of X = X --> 1;
hence thesis by A1,C0SP1:8;
end;
reserve X for compact non empty TopSpace;
reserve f,g,h for RealMap of X;
theorem Th8:
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
proof
let A be Algebra, A1,A2 be Subalgebra of A;
assume A1: the carrier of A1 c= the carrier of A2;
set CA1 = the carrier of A1;
set CA2 = the carrier of A2;
set AA = the addF of A;
set mA = the multF of A;
set MA = the Mult of A;
A2:0.A1 = 0.A & 0.A2 = 0.A & 1.A1 = 1.A & 1.A2 = 1.A by C0SP1:def 9;
A3:the addF of A1 = (the addF of A2)||the carrier of A1
proof
the addF of A1 = AA||CA1 & the addF of A2 = AA||CA2 &
[:CA1,CA1:] c= [:CA2,CA2:] by A1,C0SP1:def 9,ZFMISC_1:119;
hence thesis by FUNCT_1:82;
end;
A4:the multF of A1 = (the multF of A2)||the carrier of A1
proof
the multF of A1 = mA||CA1 & the multF of A2 = mA||CA2 &
[:CA1,CA1:] c= [:CA2,CA2:] by A1,C0SP1:def 9,ZFMISC_1:119;
hence thesis by FUNCT_1:82;
end;
the Mult of A1 = (the Mult of A2) | [:REAL,CA1:]
proof
the Mult of A1 = MA|[:REAL,CA1:] & the Mult of A2 = MA|[:REAL,CA2:] &
[:REAL,CA1:] c= [:REAL,CA2:] by A1,C0SP1:def 9,ZFMISC_1:119;
hence thesis by FUNCT_1:82;
end;
hence thesis by A1,A2,A3,A4,C0SP1:def 9;
end;
Lm1:
for x being set st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X
proof
let x be set;
assume x in ContinuousFunctions X; then
consider h be continuous RealMap of X such that
A1: x=h;
A2:h is bounded_above & h is bounded_below by SEQ_2:def 8; then
consider r1 being real number such that
A3: for y being set st y in dom h holds h.y < r1 by SEQ_2:def 1;
A4: (the carrier of X) /\ dom h c= dom h by XBOOLE_1:17; then
for y being set st y in (the carrier of X) /\ dom h holds h.y<=r1
by A3; then
A5: h|(the carrier of X) is bounded_above by RFUNCT_1:87;
consider r2 being real number such that
A6: for y being set st y in dom h holds r2 Function of (ContinuousFunctions X),REAL
equals
(BoundedFunctionsNorm the carrier of X)|(ContinuousFunctions X);
correctness
proof
for x being set st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X by Lm1; then
ContinuousFunctions X c= BoundedFunctions the carrier of X by TARSKI:def 3;
hence thesis by FUNCT_2:38;
end;
end;
definition let X;
func R_Normed_Algebra_of_ContinuousFunctions X -> Normed_AlgebraStr equals
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 #);
correctness;
end;
registration let X;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> strict non empty;
correctness;
end;
Lm2:
now let X;
set F = R_Normed_Algebra_of_ContinuousFunctions X;
let x,e be Element of F;
assume
A1: e = One_(ContinuousFunctions X,RAlgebra the carrier of X);
set X1 = ContinuousFunctions X;
reconsider f = x as Element of X1;
1_RAlgebra the carrier of X = X-->1
.= 1_R_Algebra_of_ContinuousFunctions X by Th7; then
A2:[f,1_RAlgebra the carrier of X] in [:X1,X1:] &
[1_RAlgebra the carrier of X,f] in [:X1,X1:] by ZFMISC_1:106;
x * e = (mult_(X1,RAlgebra the carrier of X))
.(f,1_RAlgebra the carrier of X) by A1,C0SP1:def 8; then
x * e = ((the multF of RAlgebra the carrier of X)||X1)
.(f,1_RAlgebra the carrier of X) by C0SP1:def 6; then
x * e = f * 1_RAlgebra the carrier of X by A2,FUNCT_1:72;
hence x * e = x by VECTSP_1:def 13;
e * x = (mult_(X1,RAlgebra the carrier of X))
.(1_RAlgebra the carrier of X,f) by A1,C0SP1:def 8; then
e * x = ((the multF of RAlgebra the carrier of X)||X1)
.(1_RAlgebra the carrier of X,f) by C0SP1:def 6; then
e * x = (1_RAlgebra the carrier of X )* f by A2,FUNCT_1:72;
hence e * x = x by VECTSP_1:def 13;
end;
registration let X;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> unital;
correctness
proof
reconsider e = One_(ContinuousFunctions X, RAlgebra the carrier of X) as
Element of R_Normed_Algebra_of_ContinuousFunctions X;
take e;
thus thesis by Lm2;
end;
end;
theorem Th10:
for W be Normed_AlgebraStr, V be Algebra st
the AlgebraStr of W = V holds W is Algebra
proof
let W be Normed_AlgebraStr,V be Algebra such that
A1:the AlgebraStr of W = V;
reconsider W as non empty AlgebraStr by A1;
A2:for x,y being VECTOR of W holds x + y = y + x
proof
let x,y be VECTOR of W;
reconsider x1 = x, y1 = y as VECTOR of V by A1;
x + y = x1+y1 by A1; then
x + y =y1 + x1;
hence x + y = y + x by A1;
end;
A3:for x,y,z being VECTOR of W holds (x + y) + z = x + (y + z)
proof
let x,y,z be VECTOR of W;
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1;
(x + y) + z = (x1 + y1) + z1 by A1; then
(x + y) + z = x1 + (y1 + z1) by RLVECT_1:def 6;
hence (x + y) + z = x + (y + z) by A1;
end;
A4:for x being VECTOR of W holds x + 0.W = x
proof
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1;
x + 0.W = y + 0.V by A1;
hence x + 0.W = x by RLVECT_1:10;
end;
A5:for x being Element of W holds x is right_complementable
proof
let x be Element of W;
reconsider x1 = x as Element of V by A1;
consider v be Element of V such that
A6: x1 + v = 0.V by ALGSTR_0:def 11;
reconsider y = v as Element of W by A1;
x + y = 0.W by A6,A1;
hence thesis by ALGSTR_0:def 11;
end;
A7:for v,w being Element of W holds v * w = w * v
proof
let v,w be Element of W;
reconsider v1 = v, w1 = w as Element of V by A1;
v * w = v1*w1 by A1; then
v * w = w1*v1;
hence v * w =w*v by A1;
end;
A8:for a,b,x being Element of W holds (a * b) * x = a * (b * x)
proof
let a,b,x be Element of W;
reconsider y = x, a1 = a, b1 = b as Element of V by A1;
(a * b) * x = (a1 * b1) * y by A1; then
(a * b) * x = a1 * (b1 * y) by GROUP_1:def 4;
hence (a * b) * x = a * (b * x) by A1;
end;
A9:W is right_unital
proof
let x be Element of W;
reconsider x1 = x as Element of V by A1;
x*1.W = x1*1.V by A1;
hence x*1.W = x by VECTSP_1:def 13;
end;
A10:W is right-distributive
proof
let x,y,z being Element of W;
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1;
x*(y+z) = x1*(y1+z1) by A1; then
x*(y+z) = x1*y1 + x1*z1 by VECTSP_1:def 11;
hence x*(y+z) = x*y + x*z by A1;
end;
W is vector-distributive scalar-distributive scalar-associative
vector-associative
proof
thus W is vector-distributive
proof
let a be real number;
let x,y being Element of W;
reconsider x1 = x, y1 = y as Element of V by A1;
a*(x+y) = a*(x1+y1) by A1; then
a*(x+y) = a*x1 + a*y1 by RLVECT_1:def 8;
hence a*(x+y) = a*x + a*y by A1;
end;
thus W is scalar-distributive
proof
let a,b be real number;
let x being Element of W;
reconsider x1 = x as Element of V by A1;
(a+b)*x = (a+b)*x1 by A1; then
(a+b)*x = a*x1 + b*x1 by RLVECT_1:def 9;
hence (a+b)*x =a*x + b*x by A1;
end;
thus W is scalar-associative
proof
let a,b be real number;
let x being Element of W;
reconsider x1 = x as Element of V by A1;
(a*b)*x = (a*b)*x1 by A1; then
(a*b)*x = a*(b*x1) by RLVECT_1:def 10;
hence (a*b)*x = a*(b*x) by A1;
end;
let x,y being Element of W;
let a be Real;
reconsider x1 = x, y1 = y as Element of V by A1;
a*(x*y) = a*(x1*y1) by A1; then
a*(x*y) = (a*x1)*y1 by FUNCSDOM:def 20;
hence a*(x*y) = (a*x)*y by A1;
end;
hence thesis by A2,A3,A4,A5,A7,A8,A9,A10
,ALGSTR_0:def 16,GROUP_1:def 4,def 16
,RLVECT_1:def 5,def 6,def 7;
end;
reserve F,G,H for Point of R_Normed_Algebra_of_ContinuousFunctions X;
Lm3:
for x be Point of R_Normed_Algebra_of_ContinuousFunctions X,
y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
st x=y holds ||.x.||= ||.y.||
by FUNCT_1:72;
Lm4:
for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
st x1=y1 & x2=y2 holds x1+x2=y1+y2
proof
let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions
the carrier of X;
assume A1: x1=y1 & x2=y2;
thus x1+x2 = ((the addF of RAlgebra the carrier of X)
||(ContinuousFunctions X)).([x1,x2]) by C0SP1:def 5
.= (the addF of RAlgebra the carrier of X).([x1,x2]) by FUNCT_1:72
.= ((the addF of RAlgebra the carrier of X)
||(BoundedFunctions the carrier of X)).([y1,y2]) by A1,FUNCT_1:72
.=y1+y2 by C0SP1:def 5;
end;
Lm5:
for a be Real,x be Point of R_Normed_Algebra_of_ContinuousFunctions X,
y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
st x=y holds a*x=a*y
proof
let a be Real, x be Point of R_Normed_Algebra_of_ContinuousFunctions X,
y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume A1: x=y;
thus a*x = ((the Mult of RAlgebra the carrier of X)|
[:REAL,(ContinuousFunctions X):]).([a,x]) by C0SP1:def 11
.= (the Mult of RAlgebra the carrier of X).([a,x]) by FUNCT_1:72
.= ((the Mult of RAlgebra the carrier of X)
|[:REAL,(BoundedFunctions the carrier of X):]).([a,y]) by A1,FUNCT_1:72
.=a*y by C0SP1:def 11;
end;
Lm6:
for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
st x1=y1 & x2=y2 holds x1*x2=y1*y2
proof
let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume A1: x1=y1 & x2=y2;
thus x1*x2 = ((the multF of RAlgebra the carrier of X)||
(ContinuousFunctions X)).([x1,x2]) by C0SP1:def 6
.= (the multF of RAlgebra the carrier of X).([x1,x2]) by FUNCT_1:72
.= ((the multF of RAlgebra the carrier of X)
||(BoundedFunctions the carrier of X)).([y1,y2]) by A1,FUNCT_1:72
.=y1*y2 by C0SP1:def 6;
end;
registration let X;
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;
coherence
proof
1.(R_Normed_Algebra_of_ContinuousFunctions X)
= 1_R_Algebra_of_ContinuousFunctions X;
hence thesis by Th10;
end;
end;
theorem Th11:
(Mult_(ContinuousFunctions X, RAlgebra the carrier of X)).(1,F) = F
proof
set X1 = ContinuousFunctions X;
reconsider f1 = F as Element of X1;
A1:[1,f1] in [:REAL,X1:] by ZFMISC_1:106;
thus (Mult_(ContinuousFunctions X, RAlgebra the carrier of X)).(1,F)
= ((the Mult of RAlgebra the carrier of X)| [:REAL,X1:]).(1,f1)
by C0SP1:def 11
.= (the Mult of RAlgebra the carrier of X).(1,f1) by A1,FUNCT_1:72
.= F by FUNCSDOM:23;
end;
registration let X;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence
proof
for v being VECTOR of R_Normed_Algebra_of_ContinuousFunctions X
holds 1 * v = v by Th11;
hence thesis by RLVECT_1:def 11;
end;
end;
theorem Th12:
X --> 0 = 0.R_Normed_Algebra_of_ContinuousFunctions X
proof
X-->0 = 0.R_Algebra_of_ContinuousFunctions X by Th6;
hence thesis;
end;
Lm7:
0.R_Normed_Algebra_of_ContinuousFunctions X
= 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X
proof
thus 0.R_Normed_Algebra_of_ContinuousFunctions X = X-->0 by Th12
.= 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:26;
end;
Lm8:
1.R_Normed_Algebra_of_ContinuousFunctions X
= 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X
proof
thus 1.R_Normed_Algebra_of_ContinuousFunctions X
=1_R_Algebra_of_ContinuousFunctions X
.= X-->1 by Th7
.= 1_R_Algebra_of_BoundedFunctions the carrier of X by C0SP1:16
.= 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X;
end;
theorem
0 <= ||.F.||
proof
reconsider F1=F as Point of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
||.F.|| =||.F1.|| by FUNCT_1:72;
hence thesis by C0SP1:28;
end;
theorem
F = 0.R_Normed_Algebra_of_ContinuousFunctions X implies 0 = ||.F.||
proof
assume A1: F = 0.R_Normed_Algebra_of_ContinuousFunctions X;
reconsider F1=F as Point of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A2: ||.F.|| =||.F1.|| by FUNCT_1:72;
F= X--> 0 by A1,Th12; then
F1 = 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:26;
hence thesis by A2,C0SP1:29;
end;
theorem Th15:
f=F & g=G & h=H implies
(H = F+G iff for x be Element of X holds h.x = f.x + g.x)
proof
reconsider f1=F, g1=G, h1=H as VECTOR of R_Algebra_of_ContinuousFunctions X;
H=F+G iff h1=f1+g1;
hence thesis by Th3;
end;
theorem
f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x )
proof
reconsider f1=F, g1=G as VECTOR of R_Algebra_of_ContinuousFunctions X;
G=a*F iff g1=a*f1;
hence thesis by Th4;
end;
theorem
f=F & g=G & h=H implies
(H = F*G iff for x be Element of X holds h.x = f.x * g.x)
proof
reconsider f1=F, g1=G, h1=H as VECTOR of R_Algebra_of_ContinuousFunctions X;
H=F*G iff h1=f1*g1;
hence thesis by Th5;
end;
theorem Th18:
( ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_ContinuousFunctions X ) &
||.a*F.|| = abs a * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||
proof
reconsider F1=F, G1=G as Point of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A1: ||.F.|| =||.F1.|| by FUNCT_1:72;
A2: ||.G.|| =||.G1.|| by FUNCT_1:72;
A3: ||.F+G.|| =||.F1+G1.|| by Lm4,Lm3;
||.F1.|| = 0 iff
F1=0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:33;
hence ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_ContinuousFunctions X
by Lm7,FUNCT_1:72;
thus ||.a*F.|| = ||.a*F1.|| by Lm5,Lm3
.=abs a * ||.F1.|| by C0SP1:33
.=abs a * ||.F.|| by FUNCT_1:72;
thus ||.F+G.|| <= ||.F.|| + ||.G.|| by A1,A2,A3,C0SP1:33;
end;
registration let X;
cluster R_Normed_Algebra_of_ContinuousFunctions X ->
reflexive discerning RealNormSpace-like;
coherence
proof set R = R_Normed_Algebra_of_ContinuousFunctions X;
thus ||.0.R.|| = 0 by Th18;
for x,y being Point of R_Normed_Algebra_of_ContinuousFunctions X
for a be Real holds
( ||.x.|| = 0 iff x = 0.R_Normed_Algebra_of_ContinuousFunctions(X) ) &
||.a*x.|| = abs(a) * ||.x.|| &
||.x+y.|| <= ||.x.|| + ||.y.|| by Th18;
hence thesis by NORMSP_0:def 5,NORMSP_1:def 2;
end;
end;
Lm9:
for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
st x1=y1 & x2=y2 holds x1-x2=y1-y2
proof
let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions X,
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume A1: x1=y1 & x2=y2;
-x2=(-1)*x2 by RLVECT_1:29
.=(-1)*y2 by A1,Lm5
.= -y2 by RLVECT_1:29;
hence x1-x2 =y1-y2 by A1,Lm4;
end;
theorem
f=F & g=G & h=H implies
(H = F-G iff (for x be Element of X holds h.x = f.x - g.x))
proof
assume A1: f=F & g=G & h=H;
A2:now assume H=F-G; then
H+G=F-(G-G) by RLVECT_1:43; then
H+G=F-0.R_Normed_Algebra_of_ContinuousFunctions X by RLVECT_1:28; then
A3: H+G=F by RLVECT_1:26;
now let x be Element of X;
f.x=h.x + g.x by A1,A3,Th15;
hence f.x-g.x=h.x;
end;
hence for x be Element of X holds h.x = f.x - g.x;
end;
now assume
A4: for x be Element of X holds h.x = f.x - g.x;
now let x be Element of X;
h.x = f.x - g.x by A4;
hence h.x + g.x= f.x;
end; then
F=H+G by A1,Th15; then
F-G=H+(G-G) by RLVECT_1:def 6; then
F-G=H+0.R_Normed_Algebra_of_ContinuousFunctions X by RLVECT_1:28;
hence F-G=H by RLVECT_1:10;
end;
hence thesis by A2;
end;
theorem Th20:
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
proof
let X be RealBanachSpace, Y be Subset of X, seq be sequence of X;
assume
A1: Y is closed & rng seq c= Y & seq is Cauchy_sequence_by_Norm;
hence seq is convergent by LOPBAN_1:def 16;
hence thesis by A1,NFCONT_1:def 5;
end;
theorem Th21:
for Y be Subset of R_Normed_Algebra_of_BoundedFunctions the carrier of X st
Y = ContinuousFunctions X holds Y is closed
proof
let Y be Subset of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume A1: Y = ContinuousFunctions X;
now let seq be sequence of
R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume A2: rng seq c= Y & seq is convergent;
lim seq in BoundedFunctions the carrier of X; then
consider f be Function of (the carrier of X),REAL such that
A3: f=lim seq & f|(the carrier of X) is bounded;
now let z be set;
assume z in BoundedFunctions (the carrier of X); then
ex f be RealMap of X st f=z & f|(the carrier of X) is bounded;
hence z in PFuncs(the carrier of X,REAL) by PARTFUN1:119;
end; then
BoundedFunctions (the carrier of X) c= PFuncs(the carrier of X,REAL)
by TARSKI:def 3; then
reconsider H = seq as Functional_Sequence of (the carrier of X),REAL
by FUNCT_2:9;
A4: for p be Real st p>0 ex k be Element of NAT st
for n be Element of NAT, x be set st
n>=k & x in the carrier of X holds abs((H.n).x - f.x) < p
proof
let p be Real;
assume p>0; then
consider k be Element of NAT such that
A5: for n be Element of NAT st n >= k holds
||.seq.n - lim seq.|| < p by A2,NORMSP_1:def 11;
take k;
hereby let n be Element of NAT, x be set;
assume A6: n>=k & x in the carrier of X; then
A7: ||.seq.n - lim seq.|| < p by A5;
seq.n - lim seq in BoundedFunctions the carrier of X; then
consider g be RealMap of X such that
A8: g=seq.n - lim seq & g|(the carrier of X) is bounded;
seq.n in BoundedFunctions the carrier of X; then
consider s be RealMap of X such that
A9: s=seq.n & s|(the carrier of X) is bounded;
reconsider x0 = x as Element of the carrier of X by A6;
A10: g.x0= s.x0-f.x0 by A8,A9,A3,C0SP1:35;
abs(g.x0) <= ||.seq.n - lim seq.|| by A8,C0SP1:27;
hence abs((H.n).x - f.x) < p by A10,A9,A7,XXREAL_0:2;
end;
end;
f is continuous
proof
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
proof
let x be Point of X,V be Subset of REAL;
set r=f.x;
assume f.x in V & V is open; then
consider r0 being real number such that
A11: 0=k & x in the carrier of X holds
abs((H.n).x - f.x) < r0/3 by A4,A11,XREAL_1:224;
A13: abs((H.k).x - f.x) < r0/3 by A12;
k in NAT; then
k in dom seq by NORMSP_1:17; then
H.k in rng seq by FUNCT_1:def 5; then
H.k in Y by A2; then
consider h be continuous RealMap of X such that
A14: H.k=h by A1;
set r1 = h.x;
set G1 = ]. r1-r0/3,r1+r0/3 .[;
A15: r10;
consider k be Element of NAT such that
A4: for n,m be Element of NAT st n >= k & m >= k holds
||. vseq.n - vseq.m .|| < e by A1,A3,RSSPACE3:10;
take k;
now let n,m be Element of NAT;
assume n >= k & m >= k; then
||. vseq.n - vseq.m .|| < e by A4;
hence ||. vseq1.n - vseq1.m .|| < e by Lm9,Lm3;
end;
hence for n,m be Element of NAT st n >= k & m >= k holds
||. vseq1.n - vseq1.m .|| < e;
end; then
A5:vseq1 is Cauchy_sequence_by_Norm by RSSPACE3:10; then
A6:vseq1 is convergent by C0SP1:36;
reconsider Y = ContinuousFunctions X as Subset of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by A2,TARSKI:def 3;
A7:rng vseq c= ContinuousFunctions X;
Y is closed by Th21;then
reconsider tv=lim vseq1 as Point of
R_Normed_Algebra_of_ContinuousFunctions X by A7,A5,Th20;
for e be Real st e > 0 ex k be Element of NAT st for n be Element of NAT st
n >= k holds ||.vseq.n - tv.|| < e
proof
let e be Real;
assume e > 0; then
consider k be Element of NAT such that
A8: for n be Element of NAT st n >= k holds
||.vseq1.n - lim vseq1.|| < e by A6,NORMSP_1:def 11;
take k;
now let n be Element of NAT;
assume n >= k; then
||.vseq1.n-lim vseq1.|| < e by A8;
hence ||.vseq.n-tv.|| < e by Lm9,Lm3;
end;
hence for n be Element of NAT st n >= k holds ||.vseq.n - tv.|| < e;
end;
hence thesis by NORMSP_1:def 9;
end;
registration let X;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> complete;
coherence
proof
for seq be sequence of R_Normed_Algebra_of_ContinuousFunctions X st
seq is Cauchy_sequence_by_Norm holds seq is convergent by Th22;
hence thesis by LOPBAN_1:def 16;
end;
end;
registration let X;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> Banach_Algebra-like;
coherence
proof
set B = R_Normed_Algebra_of_ContinuousFunctions X;
A1:now let f,g be Element of B;
reconsider f1=f, g1=g as Point of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A2: ||.f.|| =||.f1.|| & ||.g.|| =||.g1.|| & ||.f*g.|| =||.f1*g1.||
by Lm6,Lm3;
R_Normed_Algebra_of_BoundedFunctions the carrier of X is
Banach_Algebra-like_1 by C0SP1:38;
hence ||. f*g .|| <= ||.f.|| * ||.g.|| by A2,LOPBAN_2:def 9;
end;
A3: R_Normed_Algebra_of_BoundedFunctions the carrier of X
is Banach_Algebra-like_2 by C0SP1:38;
A4:||. 1.B .||=||. 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X.||
by Lm8,Lm3
.= 1 by A3,LOPBAN_2:def 10;
A5:now let a be Real, f,g be Element of B;
reconsider f1=f, g1=g as Point of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A6: a*g1=a*g by Lm5;
A7: f*g=f1*g1 by Lm6;
A8: R_Normed_Algebra_of_BoundedFunctions the carrier of X is
Banach_Algebra-like_3 by C0SP1:38;
a*(f*g) =a*(f1*g1) by A7,Lm5; then
a*(f*g) =f1*(a*g1) by A8,LOPBAN_2:def 11;
hence a*(f*g) =f*(a*g) by A6,Lm6;
end;
now let f,g,h be Element of B;
reconsider f1=f, g1=g, h1=h as Point of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A9: g+h = g1+h1 by Lm4;
A10: g*f = g1*f1 & h*f = h1*f1 by Lm6;
A11: R_Normed_Algebra_of_BoundedFunctions the carrier of X is
left-distributive by C0SP1:38;
thus (g+h)*f =(g1+h1)*f1 by Lm6,A9
.= g1*f1 + h1*f1 by A11,VECTSP_1:def 12
.= g*f + h*f by Lm4,A10;
end;
then B is Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
left-distributive left_unital complete Normed_Algebra
by A1,A4,A5,LOPBAN_2:def 9,def 10,def 11,VECTSP_1:def 12;
hence thesis;
end;
end;