:: Banach Algebra of Bounded Functionals
:: by Yasunari Shidama , Hikofumi Suzuki and Noboru Endou
::
:: Received March 3, 2008
:: Copyright (c) 2008-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 NUMBERS, XBOOLE_0, ALGSTR_0, SUBSET_1, ARYTM_1, IDEAL_1, ARYTM_3,
FUNCSDOM, STRUCT_0, TARSKI, REALSET1, MESFUNC1, SUPINF_2, BINOP_1,
FUNCT_1, ZFMISC_1, RELAT_1, RLVECT_1, VECTSP_1, LATTICES, RSSPACE,
GROUP_1, REAL_1, POLYALG1, CARD_1, RSSPACE4, XXREAL_2, FUNCOP_1, FUNCT_2,
VALUED_1, LOPBAN_1, COMPLEX1, XXREAL_0, SEQ_4, ORDINAL2, LOPBAN_2,
PRE_TOPC, NORMSP_1, NAT_1, RSSPACE3, SEQ_2, SEQ_1, REWRITE1, C0SP1,
METRIC_1, RELAT_2, FUNCT_7, ASYMPT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
XCMPLX_0, XREAL_0, COMPLEX1, XXREAL_0, XXREAL_2, STRUCT_0, ALGSTR_0,
REAL_1, REALSET1, FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, RELSET_1,
PRE_TOPC, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM, PARTFUN1, IDEAL_1,
RSSPACE3, VALUED_1, SEQ_1, SEQ_2, SEQ_4, FUNCOP_1, NORMSP_0, NORMSP_1,
LOPBAN_1, LOPBAN_2;
constructors REAL_1, REALSET1, RSSPACE3, COMPLEX1, BINOP_2, LOPBAN_2, SEQ_2,
IDEAL_1, SEQ_4, RELSET_1, COMSEQ_2, SEQ_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, XREAL_0, REALSET1, ALGSTR_0,
NUMBERS, ORDINAL1, MEMBERED, FUNCSDOM, XXREAL_0, RLVECT_1, VECTSP_1,
VECTSP_2, FUNCT_2, VALUED_0, VALUED_1, LOPBAN_2, FUNCOP_1, SEQ_4,
RFUNCT_1, RELSET_1, SEQ_1, SEQ_2;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin :: Some properties of Rings
definition
let V be non empty addLoopStr;
let V1 be Subset of V;
attr V1 is having-inverse means
:: C0SP1:def 1
for v be Element of V st v in V1 holds -v in V1;
end;
definition
let V be non empty addLoopStr;
let V1 be Subset of V;
attr V1 is additively-closed means
:: C0SP1:def 2
V1 is add-closed having-inverse;
end;
registration
let V be non empty addLoopStr;
cluster [#]V -> add-closed having-inverse;
end;
registration
let V be non empty doubleLoopStr;
cluster additively-closed -> add-closed having-inverse for Subset of V;
cluster add-closed having-inverse -> additively-closed for Subset of V;
end;
registration
let V be non empty addLoopStr;
cluster add-closed having-inverse non empty for Subset of V;
end;
definition
let V be Ring;
mode Subring of V -> Ring means
:: C0SP1:def 3
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
& 1.it=1.V & 0.it = 0.V;
end;
reserve X for non empty set;
reserve x for Element of X;
reserve d1,d2 for Element of X;
reserve A for BinOp of X;
reserve M for Function of [:X,X:],X;
reserve V for Ring;
reserve V1 for Subset of V;
theorem :: C0SP1:1
V1 = X & A = (the addF of V)||V1 & M = (the multF of V)||V1 & d1
= 1.V & d2 = 0.V & V1 is having-inverse implies doubleLoopStr (# X,A,M,d1,d2 #)
is Subring of V;
registration
let V be Ring;
cluster strict for Subring of V;
end;
definition
let V be non empty multLoopStr_0;
let V1 be Subset of V;
attr V1 is multiplicatively-closed means
:: C0SP1:def 4
1.V in V1 & for v,u be Element of V st v in V1 & u in V1 holds v * u in V1;
end;
definition
let V be non empty addLoopStr, V1 be Subset of V such that
V1 is add-closed non empty;
func Add_(V1,V) -> BinOp of V1 equals
:: C0SP1:def 5
(the addF of V)||V1;
end;
definition
let V be non empty multLoopStr_0, V1 be Subset of V such that
V1 is multiplicatively-closed non empty;
func mult_(V1,V) -> BinOp of V1 equals
:: C0SP1:def 6
(the multF of V)||V1;
end;
definition
let V be add-associative right_zeroed right_complementable non empty
doubleLoopStr, V1 be Subset of V such that
V1 is add-closed having-inverse non empty;
func Zero_(V1,V) -> Element of V1 equals
:: C0SP1:def 7
0.V;
end;
definition
let V be non empty multLoopStr_0, V1 be Subset of V such that
V1 is multiplicatively-closed non empty;
func One_(V1,V) -> Element of V1 equals
:: C0SP1:def 8
1.V;
end;
theorem :: C0SP1:2
V1 is additively-closed multiplicatively-closed non empty implies
doubleLoopStr(# V1,Add_(V1,V),mult_(V1,V),One_(V1,V),Zero_(V1,V) #) is Ring;
begin :: Some properties of Algebras
reserve V for Algebra;
reserve V1 for Subset of V;
reserve MR for Function of [:REAL,X:],X;
reserve a for Real;
definition
let V be Algebra;
mode Subalgebra of V -> Algebra means
:: C0SP1:def 9
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)
| [:REAL,the carrier of it:] & 1.it = 1.V & 0.it = 0.V;
end;
theorem :: C0SP1:3
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) | [:REAL,V1:] & V1 is having-inverse
implies AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V;
registration
let V be Algebra;
cluster strict for Subalgebra of V;
end;
definition
let V be Algebra, V1 be Subset of V;
attr V1 is additively-linearly-closed means
:: C0SP1:def 10
V1 is add-closed
having-inverse & for a be Real, v be Element of V st v in V1 holds a * v in V1;
end;
registration
let V be Algebra;
cluster additively-linearly-closed -> additively-closed for Subset of V;
end;
definition
let V be Algebra, V1 be Subset of V such that
V1 is additively-linearly-closed non empty;
func Mult_(V1,V) -> Function of [:REAL,V1:], V1 equals
:: C0SP1:def 11
(the Mult of V) | [:REAL,V1:];
end;
definition
let V be non empty RLSStruct;
attr V is scalar-mult-cancelable means
:: C0SP1:def 12
for a be Real, v be Element of V st a*v=0.V holds a=0 or v=0.V;
end;
theorem :: C0SP1:4
for V being add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
vector-associative non empty AlgebraStr, a be Real holds a*0.V = 0.V;
theorem :: C0SP1:5
for V being Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
vector-associative non empty AlgebraStr st V is scalar-mult-cancelable
holds V is RealLinearSpace;
theorem :: C0SP1:6
V1 is additively-linearly-closed multiplicatively-closed non
empty implies AlgebraStr(# V1,mult_(V1,V), Add_(V1,V), Mult_(V1,V), One_(V1,V),
Zero_(V1,V) #) is Subalgebra of V;
registration
let X be non empty set;
cluster RAlgebra X -> Abelian add-associative right_zeroed
right_complementable commutative associative right_unital right-distributive
vector-distributive scalar-distributive scalar-associative
vector-associative;
end;
theorem :: C0SP1:7
RAlgebra X is RealLinearSpace;
theorem :: C0SP1:8
for V be Algebra, V1 be Subalgebra 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 Real st v1=v holds a*v1=a*v )
& 1_V1 = 1_V & 0.V1=0.V;
begin :: Banach Algebra of Bounded Functionals
definition
let X be non empty set;
func BoundedFunctions X -> non empty Subset of RAlgebra X equals
:: C0SP1:def 13
{ f where f
is Function of X,REAL : f|X is bounded };
end;
theorem :: C0SP1:9
BoundedFunctions X is additively-linearly-closed multiplicatively-closed;
registration
let X;
cluster BoundedFunctions X -> additively-linearly-closed
multiplicatively-closed;
end;
definition
let X be non empty set;
func R_Algebra_of_BoundedFunctions X -> Algebra equals
:: C0SP1:def 14
AlgebraStr (#
BoundedFunctions X, mult_(BoundedFunctions X,RAlgebra X), Add_(BoundedFunctions
X,RAlgebra X), Mult_(BoundedFunctions X,RAlgebra X), One_(BoundedFunctions X,
RAlgebra X), Zero_(BoundedFunctions X,RAlgebra X) #);
end;
theorem :: C0SP1:10
R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X;
theorem :: C0SP1:11
R_Algebra_of_BoundedFunctions X is RealLinearSpace;
reserve F,G,H for VECTOR of R_Algebra_of_BoundedFunctions X;
reserve f,g,h for Function of X,REAL;
theorem :: C0SP1:12
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 :: C0SP1:13
f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x );
theorem :: C0SP1:14
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 :: C0SP1:15
0.R_Algebra_of_BoundedFunctions X = X -->0;
theorem :: C0SP1:16
1_R_Algebra_of_BoundedFunctions X = X -->1;
definition
let X be non empty set, F be object such that
F in BoundedFunctions X;
func modetrans(F,X) -> Function of X,REAL means
:: C0SP1:def 15
it=F & it|X is bounded;
end;
definition
let X be non empty set, f be Function of X,REAL;
func PreNorms f -> non empty Subset of REAL equals
:: C0SP1:def 16
the set of all |.f.x.| where x is Element of X ;
end;
theorem :: C0SP1:17
f|X is bounded implies PreNorms f is bounded_above;
theorem :: C0SP1:18
f|X is bounded iff PreNorms f is bounded_above;
definition
let X be non empty set;
func BoundedFunctionsNorm X -> Function of BoundedFunctions X,REAL means
:: C0SP1:def 17
for x be object st x in BoundedFunctions X
holds it.x = upper_bound PreNorms(modetrans(x,X));
end;
theorem :: C0SP1:19
f|X is bounded implies modetrans(f,X) = f;
theorem :: C0SP1:20
f|X is bounded implies (BoundedFunctionsNorm X).f = upper_bound PreNorms f;
definition
let X be non empty set;
func R_Normed_Algebra_of_BoundedFunctions X -> Normed_AlgebraStr equals
:: C0SP1:def 18
Normed_AlgebraStr (# BoundedFunctions X, mult_(BoundedFunctions X,RAlgebra X),
Add_(BoundedFunctions X,RAlgebra X), Mult_(BoundedFunctions X,RAlgebra X), One_
(BoundedFunctions X,RAlgebra X), Zero_(BoundedFunctions X,RAlgebra X),
BoundedFunctionsNorm X #);
end;
registration
let X be non empty set;
cluster R_Normed_Algebra_of_BoundedFunctions X -> non empty;
end;
registration
let X be non empty set;
cluster R_Normed_Algebra_of_BoundedFunctions X -> unital;
end;
theorem :: C0SP1:21
for W be Normed_AlgebraStr, V be Algebra st the AlgebraStr of W
= V holds W is Algebra;
reserve F,G,H for Point of R_Normed_Algebra_of_BoundedFunctions X;
theorem :: C0SP1:22
R_Normed_Algebra_of_BoundedFunctions X is Algebra;
theorem :: C0SP1:23
(Mult_(BoundedFunctions X,RAlgebra X)).(1,F) = F;
theorem :: C0SP1:24
R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace;
theorem :: C0SP1:25
X-->0 = 0.R_Normed_Algebra_of_BoundedFunctions X;
theorem :: C0SP1:26
f=F & f|X is bounded implies |.f.x.| <= ||.F.||;
theorem :: C0SP1:27
0 <= ||.F.||;
theorem :: C0SP1:28
F = 0.R_Normed_Algebra_of_BoundedFunctions X implies 0 = ||.F.||;
theorem :: C0SP1:29
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 :: C0SP1:30
f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x );
theorem :: C0SP1:31
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 :: C0SP1:32
( ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_BoundedFunctions X )
& ||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||;
theorem :: C0SP1:33
R_Normed_Algebra_of_BoundedFunctions X is
reflexive discerning RealNormSpace-like;
registration
let X be non empty set;
cluster R_Normed_Algebra_of_BoundedFunctions X ->
reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
end;
theorem :: C0SP1:34
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 :: C0SP1:35
for X be non empty set for seq be sequence of
R_Normed_Algebra_of_BoundedFunctions X st seq is Cauchy_sequence_by_Norm holds
seq is convergent;
theorem :: C0SP1:36
R_Normed_Algebra_of_BoundedFunctions X is RealBanachSpace;
registration
let X be non empty set;
cluster R_Normed_Algebra_of_BoundedFunctions X -> complete;
end;
registration let X;
cluster R_Normed_Algebra_of_BoundedFunctions X
-> Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
left-distributive left_unital;
end;
theorem :: C0SP1:37
R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra;