:: The {B}anach Algebra of Bounded Linear Operators
:: by Yasunari Shidama
::
:: Received January 26, 2004
:: Copyright (c) 2004-2026 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, RLVECT_1, LOPBAN_1, RELAT_1, REAL_1, FUNCT_1, ARYTM_3,
NORMSP_1, XXREAL_2, XXREAL_0, PRE_TOPC, CARD_1, SUBSET_1, RSSPACE,
BINOP_1, STRUCT_0, ALGSTR_0, XBOOLE_0, GROUP_1, SUPINF_2, MESFUNC1,
FUNCSDOM, VECTSP_1, LATTICES, RSSPACE3, REWRITE1, NAT_1, SEQ_2, ZFMISC_1,
PREPOWER, SEQ_1, COMPLEX1, SERIES_1, ARYTM_1, LOPBAN_2, NORMSP_0,
METRIC_1, RELAT_2, SEQ_4, FCONT_1;
notations XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1,
XXREAL_0, XXREAL_2, XCMPLX_0, XREAL_0, ORDINAL1, REAL_1, NAT_1, NUMBERS,
COMPLEX1, SEQ_1, SEQ_4, SERIES_1, PREPOWER, STRUCT_0, ALGSTR_0, PRE_TOPC,
RLVECT_1, GROUP_1, VECTSP_1, NORMSP_0, NORMSP_1, FUNCSDOM, RSSPACE,
RSSPACE3, LOPBAN_1;
constructors REAL_1, INT_2, BINOP_2, PREPOWER, SERIES_1, FUNCSDOM, RSSPACE3,
LOPBAN_1, VECTSP_1, SEQ_4, RELSET_1, GROUP_1, SEQ_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, RLVECT_1, VECTSP_1, FUNCSDOM, RSSPACE3, LOPBAN_1,
ALGSTR_0, VALUED_0, NORMSP_0, ORDINAL1, RSSPACE;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions STRUCT_0, GROUP_1, VECTSP_1, RLVECT_1, ALGSTR_0, FUNCSDOM,
NORMSP_0;
equalities STRUCT_0, LOPBAN_1, RLVECT_1, ALGSTR_0, NORMSP_0;
expansions STRUCT_0, GROUP_1, VECTSP_1, LOPBAN_1, RLVECT_1, FUNCSDOM,
NORMSP_0;
theorems ABSVALUE, RLVECT_1, VECTSP_1, BINOP_1, XCMPLX_0, SERIES_1, FUNCT_2,
NORMSP_1, SEQ_4, RSSPACE, RSSPACE3, LOPBAN_1, PREPOWER, STRUCT_0,
GROUP_1, XREAL_1, XXREAL_0, ALGSTR_0, XREAL_0, NORMSP_0;
schemes BINOP_1, NAT_1;
begin :: Banach Algebra of Bounded Linear Operators
theorem Th1:
for X,Y,Z be RealLinearSpace for f be LinearOperator of X,Y
for g be LinearOperator of Y,Z holds g*f is LinearOperator of X,Z
proof
let X,Y,Z be RealLinearSpace;
let f be LinearOperator of X,Y;
let g be LinearOperator of Y,Z;
A1: now
let v be VECTOR of X, a be Real;
thus (g*f).(a*v) =g.(f.(a*v)) by FUNCT_2:15
.=g.(a*f.v) by LOPBAN_1:def 5
.=a*g.(f.v) by LOPBAN_1:def 5
.=a*(g*f).(v) by FUNCT_2:15;
end;
now
let v,w be VECTOR of X;
thus (g*f).(v+w) =g.(f.(v+w)) by FUNCT_2:15
.=g.(f.v+f.w) by VECTSP_1:def 20
.=g.(f.v)+g.(f.w) by VECTSP_1:def 20
.=(g*f).(v)+g.(f.w) by FUNCT_2:15
.=(g*f).(v)+(g*f).(w) by FUNCT_2:15;
end;
hence thesis by A1,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
theorem Th2:
for X,Y,Z be RealNormSpace for f be Lipschitzian LinearOperator of X,Y
for g be Lipschitzian LinearOperator of Y,Z holds
g*f is Lipschitzian LinearOperator of X
,Z & for x be VECTOR of X holds ||.((g*f).x).|| <=(BoundedLinearOperatorsNorm(Y
,Z).g) *(BoundedLinearOperatorsNorm(X,Y).f )*||.x.|| & (
BoundedLinearOperatorsNorm(X,Z).(g*f)) <=(BoundedLinearOperatorsNorm(Y,Z).g) *(
BoundedLinearOperatorsNorm(X,Y).f)
proof
let X,Y,Z be RealNormSpace;
let f be Lipschitzian LinearOperator of X,Y;
let g be Lipschitzian LinearOperator of Y,Z;
reconsider ff=f as Point of R_NormSpace_of_BoundedLinearOperators(X,Y) by
LOPBAN_1:def 9;
reconsider gg=g as Point of R_NormSpace_of_BoundedLinearOperators(Y,Z) by
LOPBAN_1:def 9;
A1: now
let v be VECTOR of X;
0 <= ||.gg.|| by NORMSP_1:4;
then
A2: ||.gg.|| * ||.f.(v).|| <=||.gg.|| * ( ||.ff.|| * ||.v.||) by LOPBAN_1:32
,XREAL_1:64;
||.(g*f).v.|| = ||.g.(f.v).|| & ||.g.(f.(v)).|| <=||.gg.|| * ||.f.(v)
.|| by FUNCT_2:15,LOPBAN_1:32;
hence ||.(g*f).v.|| <=(||.gg.|| * ||.ff.||) * ||.v.|| by A2,XXREAL_0:2;
end;
A3: 0 <= ||.gg.|| & 0 <= ||.ff.|| by NORMSP_1:4;
then reconsider gf=g*f as Lipschitzian LinearOperator of X,Z by A1,Th1,
LOPBAN_1:def 8;
set K = ||.gg.|| * ||.ff.||;
A4: now
let t be VECTOR of X;
assume ||.t.|| <= 1;
then
A5: K*||.t.|| <=K*1 by A3,XREAL_1:64;
||.(g*f).t.|| <=K* ||.t.|| by A1;
hence ||.(g*f).t.|| <=K by A5,XXREAL_0:2;
end;
A6: now
let r be Real;
assume r in PreNorms(gf);
then ex t be VECTOR of X st r=||.gf.t.|| & ||.t.|| <= 1;
hence r <=K by A4;
end;
(for s be Real st s in PreNorms(gf) holds s <=K) implies upper_bound
PreNorms(gf) <=K by SEQ_4:45;
hence thesis by A1,A6,LOPBAN_1:30;
end;
definition
let X be RealNormSpace;
let f,g be Lipschitzian LinearOperator of X,X;
redefine func g*f -> Lipschitzian LinearOperator of X,X; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
correctness by Th2;
end;
definition
let X be RealNormSpace;
let f,g be Element of BoundedLinearOperators(X,X);
func f + g -> Element of BoundedLinearOperators(X,X) equals
Add_ (
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X) ) .(f,g);
correctness;
end;
definition
let X be RealNormSpace;
let f,g be Element of BoundedLinearOperators(X,X);
func g*f -> Element of BoundedLinearOperators(X,X) equals
modetrans(g,X,X)*modetrans(f,X,X);
correctness by LOPBAN_1:def 9;
end;
definition
let X be RealNormSpace;
let f be Element of BoundedLinearOperators(X,X);
let a be Real;
func a*f -> Element of BoundedLinearOperators(X,X) equals
Mult_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)).(a,f);
correctness
proof
reconsider a as Element of REAL by XREAL_0:def 1;
Mult_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)).(a,f)
is Element of BoundedLinearOperators(X,X);
hence thesis;
end;
end;
definition
let X be RealNormSpace;
func FuncMult(X) -> BinOp of BoundedLinearOperators(X,X) means
:Def4:
for f, g being Element of BoundedLinearOperators(X,X) holds it.(f,g) = f*g;
existence
proof
deffunc F(Element of BoundedLinearOperators(X,X), Element of
BoundedLinearOperators(X,X)) = $1*$2;
consider F being BinOp of BoundedLinearOperators(X,X) such that
A1: for x,y being Element of BoundedLinearOperators(X,X) holds F.(x,y)
= F(x,y) from BINOP_1:sch 4;
take F;
let f,g be Element of BoundedLinearOperators(X,X);
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be BinOp of BoundedLinearOperators(X,X) such that
A2: for f,g being Element of BoundedLinearOperators(X,X) holds it1.(f,
g) = f*g and
A3: for f,g being Element of BoundedLinearOperators(X,X) holds it2.(f,
g) = f*g;
now
let f,g be Element of BoundedLinearOperators(X,X);
thus it1.(f,g) = f*g by A2
.=it2.(f,g) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th3:
for X be RealNormSpace holds id (the carrier of X) is Lipschitzian
LinearOperator of X,X
proof
let X be RealNormSpace;
A1: for v,w be VECTOR of X holds
(id (the carrier of X)).(v+w)
=(id (the carrier of X)).v + (id (the carrier of X)).w;
A2: for v be VECTOR of X, a be Real holds
(id (the carrier of X)).(a*v) =a*(id (the carrier of X)).(v);
for v be VECTOR of X holds ||.id (the carrier of X).v.|| <=1* ||.v.||;
hence thesis by A1,A2,LOPBAN_1:def 5,def 8,VECTSP_1:def 20;
end;
definition
let X be RealNormSpace;
func FuncUnit(X) -> Element of BoundedLinearOperators(X,X) equals
id (the carrier of X);
coherence
proof
id (the carrier of X) is Lipschitzian LinearOperator of X,X by Th3;
hence thesis by LOPBAN_1:def 9;
end;
end;
theorem Th4:
for X be RealNormSpace for f,g,h be Lipschitzian LinearOperator of X,X
holds h = f*g iff for x be VECTOR of X holds h.x = f.(g.x)
proof
let X be RealNormSpace;
let f,g,h be Lipschitzian LinearOperator of X,X;
now
assume
A1: for x being VECTOR of X holds h.x=f.(g.x);
now
let x be VECTOR of X;
thus (f*g).x = f.(g.x) by FUNCT_2:15
.= h.x by A1;
end;
hence h = f*g by FUNCT_2:63;
end;
hence thesis by FUNCT_2:15;
end;
theorem Th5:
for X be RealNormSpace for f,g,h be Lipschitzian LinearOperator of X,X
holds f*(g*h) =(f*g)*h
proof
let X be RealNormSpace;
let f,g,h be Lipschitzian LinearOperator of X,X;
now
let x be VECTOR of X;
thus (f*(g*h)).x =f.((g*h).x) by Th4
.= f.(g.(h.x)) by Th4
.= (f*g).(h.x) by FUNCT_2:15
.= ((f*g)*h).x by Th4;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th6:
for X be RealNormSpace for f be Lipschitzian LinearOperator of X,X
holds f*(id the carrier of X) = f & (id the carrier of X )*f=f
proof
let X be RealNormSpace;
reconsider ii=(id the carrier of X) as Lipschitzian LinearOperator of X,X
by Th3;
let f be Lipschitzian LinearOperator of X,X;
A1: now
let x be VECTOR of X;
thus ( (id the carrier of X)*f).x =( ii*f).x .=ii.(f.x) by Th4
.=f.x;
end;
now
let x be VECTOR of X;
thus ( f*(id the carrier of X)).x =( f*ii).x .=f.(ii.x) by Th4
.=f.x;
end;
hence thesis by A1,FUNCT_2:63;
end;
theorem Th7:
for X be RealNormSpace for f,g,h be Element of
BoundedLinearOperators(X,X) holds f*(g*h) =(f*g)*h
proof
let X be RealNormSpace;
let f,g,h be Element of BoundedLinearOperators(X,X);
modetrans((g*h),X,X) =modetrans(g,X,X)*modetrans(h,X,X) by LOPBAN_1:def 11;
then
modetrans(f,X,X)*modetrans((g*h),X,X) =(modetrans(f,X,X)*modetrans(g,X,X
))*modetrans(h,X,X) by Th5;
hence thesis by LOPBAN_1:def 11;
end;
theorem Th8:
for X be RealNormSpace for f be Element of BoundedLinearOperators
(X,X) holds f*FuncUnit(X)= f & FuncUnit(X)*f=f
proof
let X be RealNormSpace;
let f be Element of BoundedLinearOperators(X,X);
(id the carrier of X) is Lipschitzian LinearOperator of X,X by Th3;
then (id the carrier of X) is Element of BoundedLinearOperators(X,X) by
LOPBAN_1:def 9;
then
A1: modetrans( (id (the carrier of X)),X,X) = (id the carrier of X) by
LOPBAN_1:def 11;
hence f*FuncUnit(X) =modetrans(f,X,X) by Th6
.=f by LOPBAN_1:def 11;
thus FuncUnit(X)*f =modetrans(f,X,X) by A1,Th6
.=f by LOPBAN_1:def 11;
end;
theorem Th9:
for X be RealNormSpace for f,g,h be Element of
BoundedLinearOperators(X,X) holds f *(g+h)=f*g + f*h
proof
let X be RealNormSpace;
let f,g,h be Element of BoundedLinearOperators(X,X);
set BLOP=R_NormSpace_of_BoundedLinearOperators(X,X);
set ADD=Add_(BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X
,X));
set mf=modetrans(f,X,X);
set mg=modetrans(g,X,X);
set mh=modetrans(h,X,X);
set mgh=modetrans(g+h, X,X);
ADD.(mf*mg, mf*mh) =mf*mgh
proof
reconsider fh=mf*mh as VECTOR of BLOP by LOPBAN_1:def 9;
reconsider fg=mf*mg as VECTOR of BLOP by LOPBAN_1:def 9;
reconsider k=mf*mgh as VECTOR of BLOP by LOPBAN_1:def 9;
reconsider hh = h as VECTOR of BLOP;
reconsider gg = g as VECTOR of BLOP;
A1: gg=mg & hh=mh by LOPBAN_1:def 11;
for x be VECTOR of X holds (mf*mgh).x=(mf*mg).x + (mf*mh).x
proof
let x be VECTOR of X;
g+h=gg+hh & modetrans(g+h, X,X) =g+h by LOPBAN_1:def 11;
then
A2: mgh.x=mg.x+mh.x by A1,LOPBAN_1:35;
thus (mf*mgh).x=mf.(mgh.x) by Th4
.=mf.(mg.x) +mf.(mh.x) by A2,VECTSP_1:def 20
.=(mf*mg).x+mf.(mh.x) by Th4
.=(mf*mg).x+ (mf*mh).x by Th4;
end;
then k=fg+fh by LOPBAN_1:35;
hence thesis;
end;
hence thesis;
end;
theorem Th10:
for X be RealNormSpace for f,g,h be Element of
BoundedLinearOperators(X,X) holds (g+h)*f = g*f + h*f
proof
let X be RealNormSpace;
let f,g,h be Element of BoundedLinearOperators(X,X);
set BLOP=R_NormSpace_of_BoundedLinearOperators(X,X);
set ADD=Add_(BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X
,X));
set mf=modetrans(f,X,X);
set mg=modetrans(g,X,X);
set mh=modetrans(h,X,X);
set mgh=modetrans(g+h, X,X);
ADD.(mg*mf, mh*mf) =mgh*mf
proof
reconsider hf=mh*mf as VECTOR of BLOP by LOPBAN_1:def 9;
reconsider gf=mg*mf as VECTOR of BLOP by LOPBAN_1:def 9;
reconsider k=mgh*mf as VECTOR of BLOP by LOPBAN_1:def 9;
reconsider hh = h as VECTOR of BLOP;
reconsider gg = g as VECTOR of BLOP;
A1: gg=mg & hh=mh by LOPBAN_1:def 11;
for x be VECTOR of X holds (mgh*mf).x=(mg*mf).x + (mh*mf).x
proof
let x be VECTOR of X;
g+h=gg+hh & modetrans(g+h, X,X) =g+h by LOPBAN_1:def 11;
then
A2: mgh.(mf.x)=mg.(mf.x)+mh.(mf.x) by A1,LOPBAN_1:35;
thus (mgh*mf).x=mgh.(mf.x) by Th4
.=(mg*mf).x+mh.(mf.x) by A2,Th4
.=(mg*mf).x+ (mh*mf).x by Th4;
end;
then k=gf+hf by LOPBAN_1:35;
hence thesis;
end;
hence thesis;
end;
theorem Th11:
for X be RealNormSpace for f,g be Element of
BoundedLinearOperators(X,X)
for a,b be Real holds (a*b)*(f*g)=(a*f)*(b*g)
proof
let X be RealNormSpace;
let f,g be Element of BoundedLinearOperators(X,X);
let a,b be Real;
set BLOP=R_NormSpace_of_BoundedLinearOperators(X,X);
set EXMULT=Mult_(BoundedLinearOperators(X,X),
R_VectorSpace_of_LinearOperators(X,X));
set mf=modetrans(f,X,X);
set mg=modetrans(g,X,X);
set maf=modetrans((a*f),X,X);
set mbg=modetrans(b*g,X,X);
EXMULT.(a*b,mf*mg)=maf*mbg
proof
reconsider k=(maf)*(mbg) as VECTOR of BLOP by LOPBAN_1:def 9;
reconsider fg=mf*mg as VECTOR of BLOP by LOPBAN_1:def 9;
reconsider ff = f, gg = g as VECTOR of BLOP;
A1: gg=mg by LOPBAN_1:def 11;
A2: ff=mf by LOPBAN_1:def 11;
for x be VECTOR of X holds ( (maf)*(mbg)).x=(a*b)*(mf*mg).x
proof
let x be VECTOR of X;
set y=b*mg.x;
a*f=a*ff & modetrans(a*f, X,X) =a*f by LOPBAN_1:def 11;
then
A3: maf.y=a*mf.y by A2,LOPBAN_1:36;
b*g=b*gg & modetrans(b*g, X,X) =b*g by LOPBAN_1:def 11;
then
A4: mbg.x=b*mg.x by A1,LOPBAN_1:36;
thus (maf*mbg).x=maf.(mbg.x) by Th4
.=a*(b*mf.(mg.x)) by A3,A4,LOPBAN_1:def 5
.=(a*b)*mf.(mg.x) by RLVECT_1:def 7
.=(a*b)*(mf*mg).x by Th4;
end;
then k=(a*b)*fg by LOPBAN_1:36;
hence thesis;
end;
hence thesis;
end;
theorem Th12:
for X be RealNormSpace for f,g be Element of
BoundedLinearOperators(X,X) for a be Real holds a*(f*g) =(a*f)*g
proof
let X be RealNormSpace;
let f,g be Element of BoundedLinearOperators(X,X);
let a be Real;
set RRL=RLSStruct (# BoundedLinearOperators(X,X), Zero_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), Add_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)) #);
reconsider jj=1 as Real;
reconsider gg=g as Element of RRL;
A1: (jj*g)=jj*gg .=g by RLVECT_1:def 8;
a*(f*g)=(a*jj)*(f*g) .=(a*f)*(jj*g) by Th11;
hence thesis by A1;
end;
definition
let X be RealNormSpace;
func Ring_of_BoundedLinearOperators(X) -> doubleLoopStr equals
doubleLoopStr
(# BoundedLinearOperators(X,X), Add_(BoundedLinearOperators(X,X),
R_VectorSpace_of_LinearOperators(X,X)), FuncMult(X), FuncUnit(X), Zero_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)) #);
correctness;
end;
registration
let X be RealNormSpace;
cluster Ring_of_BoundedLinearOperators(X) -> non empty strict;
coherence;
end;
Lm1: now
let X be RealNormSpace;
set F = Ring_of_BoundedLinearOperators(X);
let x, e be Element of F;
reconsider f = x as Element of BoundedLinearOperators(X,X);
assume
A1: e = FuncUnit(X);
hence x * e = f * (FuncUnit(X)) by Def4
.= x by Th8;
thus e * x = (FuncUnit(X)) * f by A1,Def4
.= x by Th8;
end;
registration
let X be RealNormSpace;
cluster Ring_of_BoundedLinearOperators(X) -> unital;
coherence
proof
reconsider e = FuncUnit(X) as Element of Ring_of_BoundedLinearOperators(X);
take e;
thus thesis by Lm1;
end;
end;
theorem Th13:
for X be RealNormSpace for x,y,z being Element of
Ring_of_BoundedLinearOperators(X) holds x+y = y+x & (x+y)+z = x+(y+z) & x+(0.
Ring_of_BoundedLinearOperators(X)) = x & (ex t being Element of
Ring_of_BoundedLinearOperators(X) st x+t= 0.Ring_of_BoundedLinearOperators(X))
& (x*y)*z = x*(y*z) & x*(1.Ring_of_BoundedLinearOperators(X)) = x & (1.
Ring_of_BoundedLinearOperators(X))*x = x & x*(y+z) = x*y + x*z & (y+z)*x = y*x
+ z*x
proof
let X be RealNormSpace;
let x,y,z be Element of Ring_of_BoundedLinearOperators(X);
set RBLOP=Ring_of_BoundedLinearOperators(X);
set BLOP=BoundedLinearOperators(X,X);
set ADD=Add_(BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X
,X));
set MULT= FuncMult(X);
set UNIT=FuncUnit(X);
set RRL=RLSStruct (# BoundedLinearOperators(X,X), Zero_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), Add_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)) #);
reconsider f=x, g=y, h=z as Element of RRL;
thus x+y =f+g .= y+x by RLVECT_1:2;
thus (x+y)+z =(f+g)+h .=f+(g+h) by RLVECT_1:def 3
.= x+(y+z);
thus x+(0.RBLOP) = f + 0.RRL .= x;
thus ex t being Element of RBLOP st x+t=(0.RBLOP)
proof
consider s be Element of RRL such that
A1: f + s = 0.RRL by ALGSTR_0:def 11;
reconsider t=s as Element of RBLOP;
take t;
thus thesis by A1;
end;
reconsider xx=x,yy=y,zz=z as Element of BLOP;
thus (x*y)*z = MULT.(xx*yy,zz) by Def4
.=(xx*yy)*zz by Def4
.=xx*(yy*zz) by Th7
.= MULT.(xx,yy*zz) by Def4
.=x*(y*z) by Def4;
thus x*(1.RBLOP) =xx*UNIT by Def4
.= x by Th8;
thus (1.RBLOP)*x =UNIT*xx by Def4
.= x by Th8;
thus x*(y+z) =xx*(yy+zz) by Def4
.=xx*yy + xx*zz by Th9
.= ADD.(xx*yy,MULT.(xx,zz)) by Def4
.= x*y + x*z by Def4;
thus (y+z)*x =(yy+zz)*xx by Def4
.=yy*xx + zz*xx by Th10
.= ADD.(yy*xx,MULT.(zz,xx)) by Def4
.= y*x + z*x by Def4;
end;
theorem Th14:
for X be RealNormSpace holds Ring_of_BoundedLinearOperators(X) is Ring
proof
let X be RealNormSpace;
set R = Ring_of_BoundedLinearOperators X;
A1: R is right_complementable
proof
let x be Element of R;
thus ex t being Element of R st x+t= 0.R by Th13;
end;
for x,y,z being Element of R holds x+y = y+x & (x+y)+z = x+(y+z) & x+(0.
Ring_of_BoundedLinearOperators(X)) = x & (ex t being Element of
Ring_of_BoundedLinearOperators(X) st x+t= 0.Ring_of_BoundedLinearOperators(X))
& (x*y)*z = x*(y*z) & x*(1.Ring_of_BoundedLinearOperators(X)) = x & (1.
Ring_of_BoundedLinearOperators(X))*x = x & x*(y+z) = x*y + x*z & (y+z)*x = y*x
+ z*x by Th13;
hence thesis by A1,GROUP_1:def 3,RLVECT_1:def 2,def 3,def 4,VECTSP_1:def 6
,def 7;
end;
registration
let X be RealNormSpace;
cluster Ring_of_BoundedLinearOperators(X) -> Abelian add-associative
right_zeroed right_complementable associative left_unital right_unital
distributive well-unital;
coherence by Th14;
end;
definition
let X be RealNormSpace;
func R_Algebra_of_BoundedLinearOperators(X) -> AlgebraStr equals
AlgebraStr
(# BoundedLinearOperators(X,X), FuncMult(X), Add_(BoundedLinearOperators(X,X),
R_VectorSpace_of_LinearOperators(X,X)), Mult_(BoundedLinearOperators(X,X),
R_VectorSpace_of_LinearOperators(X,X)), FuncUnit(X), Zero_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)) #);
correctness;
end;
registration
let X be RealNormSpace;
cluster R_Algebra_of_BoundedLinearOperators(X) -> non empty strict;
coherence;
end;
Lm2: now
let X be RealNormSpace;
set F = R_Algebra_of_BoundedLinearOperators(X);
let x, e be Element of F;
reconsider f = x as Element of BoundedLinearOperators(X,X);
assume
A1: e = FuncUnit(X);
hence x * e = f * (FuncUnit(X)) by Def4
.= x by Th8;
thus e * x = (FuncUnit(X)) * f by A1,Def4
.= x by Th8;
end;
registration
let X be RealNormSpace;
cluster R_Algebra_of_BoundedLinearOperators(X) -> unital;
coherence
proof
reconsider e = FuncUnit(X) as Element of
R_Algebra_of_BoundedLinearOperators(X);
take e;
thus thesis by Lm2;
end;
end;
theorem
for X be RealNormSpace for x,y,z being Element of
R_Algebra_of_BoundedLinearOperators(X) for a,b be Real holds x+y = y+x & (x+y)+
z = x+(y+z) & x+(0.R_Algebra_of_BoundedLinearOperators(X)) = x & (ex t being
Element of R_Algebra_of_BoundedLinearOperators(X) st x+t= 0.
R_Algebra_of_BoundedLinearOperators(X)) & (x*y)*z = x*(y*z) & x*(1.
R_Algebra_of_BoundedLinearOperators(X)) = x & (1.
R_Algebra_of_BoundedLinearOperators(X))*x = x & x*(y+z) = x*y + x*z & (y+z)*x =
y*x + z*x & a*(x*y) = (a*x)*y & a*(x+y) = a*x + a*y & (a+b)*x = a*x + b*x & (a*
b)*x = a*(b*x) & (a*b)*(x*y)=(a*x)*(b*y)
proof
let X be RealNormSpace;
let x,y,z be Element of R_Algebra_of_BoundedLinearOperators(X);
let a,b be Real;
set RBLOP=R_Algebra_of_BoundedLinearOperators(X);
set BLOP=BoundedLinearOperators(X,X);
set ADD=Add_(BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X
,X));
set MULT= FuncMult(X);
set UNIT=FuncUnit(X);
set RRL=RLSStruct (# BoundedLinearOperators(X,X), Zero_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), Add_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)) #);
reconsider f=x, g=y, h=z as Element of RRL;
thus x+y =f+g .= y+x by RLVECT_1:2;
thus (x+y)+z =(f+g)+h .=f+(g+h) by RLVECT_1:def 3
.= x+(y+z);
thus x+(0.RBLOP) = f + 0.RRL .= x;
thus ex t being Element of RBLOP st x+t=(0.RBLOP)
proof
consider s be Element of RRL such that
A1: f + s = 0.RRL by ALGSTR_0:def 11;
reconsider t=s as Element of RBLOP;
take t;
thus thesis by A1;
end;
reconsider xx=x,yy=y,zz=z as Element of BLOP;
thus (x*y)*z = MULT.(xx*yy,zz) by Def4
.=(xx*yy)*zz by Def4
.=xx*(yy*zz) by Th7
.= MULT.(xx,yy*zz) by Def4
.=x*(y*z) by Def4;
thus x*(1.RBLOP) =xx*UNIT by Def4
.= x by Th8;
thus (1.RBLOP)*x =UNIT*xx by Def4
.= x by Th8;
thus x*(y+z) =xx*(yy+zz) by Def4
.=xx*yy + xx*zz by Th9
.= ADD.(xx*yy,MULT.(xx,zz)) by Def4
.= x*y + x*z by Def4;
thus (y+z)*x =(yy+zz)*xx by Def4
.=yy*xx + zz*xx by Th10
.= ADD.(yy*xx,MULT.(zz,xx)) by Def4
.= y*x + z*x by Def4;
thus a*(x*y) = a*(xx*yy) by Def4
.= (a*xx)*(yy) by Th12
.=(a*x)*y by Def4;
thus a*(x+y) =a*(f+g) .=a*f+a*g by RLVECT_1:def 5
.=a*x+a*y;
thus (a+b)*x =(a+b)*f .=a*f+b*f by RLVECT_1:def 6
.=a*x+b*x;
thus (a*b)*x =(a*b)*f .=a*(b*f) by RLVECT_1:def 7
.=a*(b*x);
thus (a*b)*(x*y) = (a*b)*(xx*yy) by Def4
.= (a*xx)*(b*yy) by Th11
.=(a*x)*(b*y) by Def4;
end;
definition
mode BLAlgebra is Abelian add-associative right_zeroed right_complementable
associative right_unital right-distributive vector-distributive
scalar-distributive scalar-associative vector-associative
non empty AlgebraStr;
end;
registration let X be RealNormSpace;
cluster R_Algebra_of_BoundedLinearOperators X ->
Abelian add-associative right_zeroed right_complementable
associative right_unital right-distributive vector-distributive
scalar-distributive scalar-associative vector-associative strict;
coherence
proof set A = R_Algebra_of_BoundedLinearOperators X;
set BLOP=BoundedLinearOperators(X,X);
set RRL=RLSStruct (# BoundedLinearOperators(X,X), Zero_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), Add_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)) #);
set MULT= FuncMult(X);
set UNIT=FuncUnit(X);
set ADD=Add_(BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X
,X));
thus A is Abelian
proof
let x,y be Element of A;
reconsider f=x, g=y as Element of RRL;
thus x+y = f+g .= y+x by RLVECT_1:2;
end;
thus A is add-associative
proof
let x,y,z be Element of A;
reconsider f=x, g=y, h=z as Element of RRL;
thus (x+y)+z =(f+g)+h .=f+(g+h) by RLVECT_1:def 3
.= x+(y+z);
end;
thus A is right_zeroed
proof
let x be Element of A;
reconsider f=x as Element of RRL;
thus x+0.A = f + 0.RRL .= x;
end;
thus A is right_complementable
proof
let x be Element of A;
reconsider f=x as Element of RRL;
consider s be Element of RRL such that
A1: f + s = 0.RRL by ALGSTR_0:def 11;
reconsider t=s as Element of A;
take t;
thus thesis by A1;
end;
thus A is associative
proof
let x,y,z be Element of A;
reconsider xx=x,yy=y,zz=z as Element of BLOP;
thus (x*y)*z = MULT.(xx*yy,zz) by Def4
.=(xx*yy)*zz by Def4
.=xx*(yy*zz) by Th7
.= MULT.(xx,yy*zz) by Def4
.=x*(y*z) by Def4;
end;
thus A is right_unital
proof
let x be Element of A;
reconsider xx=x as Element of BLOP;
thus x*1.A =xx*UNIT by Def4
.= x by Th8;
end;
thus A is right-distributive
proof
let x,y,z be Element of A;
reconsider xx=x,yy=y,zz=z as Element of BLOP;
thus x*(y+z) =xx*(yy+zz) by Def4
.=xx*yy + xx*zz by Th9
.= ADD.(xx*yy,MULT.(xx,zz)) by Def4
.= x*y + x*z by Def4;
end;
thus A is vector-distributive
proof
let a be Real;
let x,y be Element of A;
reconsider f=x, g=y as Element of RRL;
thus a*(x+y) =a*(f+g) .=a*f+a*g by RLVECT_1:def 5
.=a*x+a*y;
end;
thus A is scalar-distributive
proof
let a,b be Real;
let x be Element of A;
reconsider f=x as Element of RRL;
thus (a+b)*x =(a+b)*f .=a*f+b*f by RLVECT_1:def 6
.=a*x+b*x;
end;
thus A is scalar-associative
proof
let a,b be Real;
let x be Element of A;
reconsider f=x as Element of RRL;
thus (a*b)*x =(a*b)*f .=a*(b*f) by RLVECT_1:def 7
.=a*(b*x);
end;
thus A is vector-associative
proof
let x,y be Element of A;
let a be Real;
reconsider xx=x,yy=y as Element of BLOP;
thus a*(x*y) = a*(xx*yy) by Def4
.= (a*xx)*yy by Th12
.=(a*x)*y by Def4;
end;
thus thesis;
end;
end;
theorem
for X be RealNormSpace holds R_Algebra_of_BoundedLinearOperators(X) is
BLAlgebra;
registration
cluster l1_Space -> complete;
coherence
by RSSPACE3:9;
end;
registration
cluster l1_Space -> non trivial;
coherence
proof
set a=1/2;
reconsider x = a GeoSeq as Real_Sequence;
A1: |.a.| = 1/2 by ABSVALUE:def 1;
defpred P[Nat] means 0 <= x.$1;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
x.(n+1) = x.n * a by PREPOWER:3;
hence thesis;
end;
A4: P[0] by PREPOWER:3;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
then x is absolutely_summable by A1,SERIES_1:24,36;
then seq_id(x) is absolutely_summable;
then reconsider v=x as VECTOR of l1_Space by RSSPACE3:6;
(seq_id v).0 = 1 by PREPOWER:3;
then v <> seq_id Zeroseq by RSSPACE:4;
hence thesis by RSSPACE3:6;
end;
end;
registration
cluster non trivial for RealBanachSpace;
existence
proof
take l1_Space;
thus thesis;
end;
end;
theorem Th17:
for X be non trivial RealNormSpace ex w be VECTOR of X st ||. w .|| = 1
proof
let X be non trivial RealNormSpace;
consider v be VECTOR of X such that
A1: v <> 0.X by STRUCT_0:def 18;
set a= ||. v .||;
reconsider w=a"*v as VECTOR of X;
take w;
A2: ||. v .|| <> 0 by A1,NORMSP_0:def 5;
then
A3: 0 < ||. v .|| by NORMSP_1:4;
A4: |.a".| =|.1*a".| .=|.1/a.| by XCMPLX_0:def 9
.=1/|.a.| by ABSVALUE:7
.=1*|.a.|" by XCMPLX_0:def 9
.=a"by A3,ABSVALUE:def 1;
thus ||.w.|| =|.a".|*||.v.|| by NORMSP_1:def 1
.=1 by A2,A4,XCMPLX_0:def 7;
end;
theorem Th18:
for X be non trivial RealNormSpace holds
BoundedLinearOperatorsNorm(X,X).(id the carrier of X) = 1
proof
let X be non trivial RealNormSpace;
consider v be VECTOR of X such that
A1: ||.v.|| = 1 by Th17;
reconsider ii=(id the carrier of X) as Lipschitzian LinearOperator of X,X
by Th3;
A2: now
let r be Real;
assume r in PreNorms(ii);
then ex t be VECTOR of X st r=||.ii.t.|| & ||.t.|| <= 1;
hence r <=1;
end;
ii.v =v;
then
A3: 1 in {||.ii.t.|| where t is VECTOR of X : ||.t.|| <= 1 } by A1;
PreNorms(ii) is non empty bounded_above by LOPBAN_1:27;
then
A4: 1 <=upper_bound PreNorms(ii) by A3,SEQ_4:def 1;
(for s be Real st s in PreNorms(ii) holds s <= 1) implies upper_bound
PreNorms(ii) <= 1 by SEQ_4:45;
then upper_bound PreNorms(ii) =1 by A2,A4,XXREAL_0:1;
hence thesis by LOPBAN_1:30;
end;
definition
struct(AlgebraStr,NORMSTR) Normed_AlgebraStr (# carrier -> set,
multF,addF -> (BinOp of the carrier),
Mult -> (Function of [:REAL,the carrier:],the carrier),
OneF,ZeroF -> Element of the carrier,
normF -> Function of the carrier, REAL#);
end;
registration
cluster non empty for Normed_AlgebraStr;
existence
proof
set A = the non empty set,m = the BinOp of A,a = the BinOp of A,M =the
Function of [:REAL,A:],A,U = the Element of A,Z = the Element of A,n =the
Function of A,REAL;
take Normed_AlgebraStr(#A,m,a,M,U,Z,n#);
thus the carrier of Normed_AlgebraStr(#A,m,a,M,U,Z,n#) is non empty;
end;
end;
definition
let X be RealNormSpace;
func R_Normed_Algebra_of_BoundedLinearOperators(X) -> Normed_AlgebraStr
equals
Normed_AlgebraStr (# BoundedLinearOperators(X,X), FuncMult(X), Add_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), FuncUnit(X
), Zero_(BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)),
BoundedLinearOperatorsNorm(X,X) #);
correctness;
end;
registration
let X be RealNormSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators(X) -> non empty strict;
coherence;
end;
Lm3: now
let X be RealNormSpace;
set F = R_Normed_Algebra_of_BoundedLinearOperators(X);
let x, e be Element of F;
reconsider f = x as Element of BoundedLinearOperators(X,X);
assume
A1: e = FuncUnit(X);
hence x * e = f * (FuncUnit(X)) by Def4
.= x by Th8;
thus e * x = (FuncUnit(X)) * f by A1,Def4
.= x by Th8;
end;
registration
let X be RealNormSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators(X) -> unital;
coherence
proof
reconsider e = FuncUnit(X) as Element of
R_Normed_Algebra_of_BoundedLinearOperators(X);
take e;
thus thesis by Lm3;
end;
end;
theorem Th19:
for X be RealNormSpace for x,y,z being Element of
R_Normed_Algebra_of_BoundedLinearOperators(X) for a,b be Real holds x+y
= y+x & (x+y)+z = x+(y+z) & x+(0.R_Normed_Algebra_of_BoundedLinearOperators(X))
= x & (ex t being Element of R_Normed_Algebra_of_BoundedLinearOperators(X) st x
+t= 0.R_Normed_Algebra_of_BoundedLinearOperators(X)) & (x*y)*z = x*(y*z) & x*(
1.R_Normed_Algebra_of_BoundedLinearOperators(X)) = x & (1.
R_Normed_Algebra_of_BoundedLinearOperators(X))*x = x & x*(y+z) = x*y + x*z & (y
+z)*x = y*x + z*x & a*(x*y) = (a*x)*y & (a*b)*(x*y)=(a*x)*(b*y) & a*(x+y) = a*x
+ a*y & (a+b)*x = a*x + b*x & (a*b)*x = a*(b*x) & 1*x =x
proof
let X be RealNormSpace;
let x,y,z be Element of R_Normed_Algebra_of_BoundedLinearOperators(X);
let a,b be Real;
reconsider a1=a, b1=b as Real;
set RBLOP=R_Normed_Algebra_of_BoundedLinearOperators(X);
set BLOP=BoundedLinearOperators(X,X);
set ADD=Add_(BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X
,X));
set MULT= FuncMult(X);
set UNIT=FuncUnit(X);
set RRL=RLSStruct (# BoundedLinearOperators(X,X), Zero_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), Add_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)) #);
reconsider f=x, g=y, h=z as Element of RRL;
thus x+y =f+g .= y+x by RLVECT_1:2;
thus (x+y)+z =(f+g)+h .=f+(g+h) by RLVECT_1:def 3
.= x+(y+z);
thus x+(0.RBLOP) = f + 0.RRL .= x;
thus ex t being Element of RBLOP st x+t=(0.RBLOP)
proof
consider s be Element of RRL such that
A1: f + s = 0.RRL by ALGSTR_0:def 11;
reconsider t=s as Element of RBLOP;
take t;
thus thesis by A1;
end;
reconsider xx=x,yy=y,zz=z as Element of BLOP;
thus (x*y)*z = MULT.(xx*yy,zz) by Def4
.=(xx*yy)*zz by Def4
.=xx*(yy*zz) by Th7
.= MULT.(xx,yy*zz) by Def4
.=x*(y*z) by Def4;
thus x*(1.RBLOP) =xx*UNIT by Def4
.= x by Th8;
thus (1.RBLOP)*x =UNIT*xx by Def4
.= x by Th8;
thus x*(y+z) =xx*(yy+zz) by Def4
.=xx*yy + xx*zz by Th9
.= ADD.(xx*yy,MULT.(xx,zz)) by Def4
.= x*y + x*z by Def4;
thus (y+z)*x =(yy+zz)*xx by Def4
.=yy*xx + zz*xx by Th10
.= ADD.(yy*xx,MULT.(zz,xx)) by Def4
.= y*x + z*x by Def4;
thus a*(x*y) = a1*(xx*yy) by Def4
.= (a1*xx)*(yy) by Th12
.=(a*x)*y by Def4;
thus (a*b)*(x*y) = (a1*b1)*(xx*yy) by Def4
.= (a1*xx)*(b1*yy) by Th11
.=(a*x)*(b*y) by Def4;
thus a*(x+y) =a*(f+g) .=a*f+a*g by RLVECT_1:def 5
.=a*x+a*y;
thus (a+b)*x =(a+b)*f .=a*f+b*f by RLVECT_1:def 6
.=a*x+b*x;
thus (a*b)*x =(a*b)*f .=a*(b*f) by RLVECT_1:def 7
.=a*(b*x);
thus 1*x =1*f .=x by RLVECT_1:def 8;
end;
theorem Th20:
for X be RealNormSpace holds R_Normed_Algebra_of_BoundedLinearOperators(X) is
reflexive discerning RealNormSpace-like Abelian
add-associative right_zeroed right_complementable associative right_unital
right-distributive vector-distributive scalar-distributive scalar-associative
vector-associative vector-distributive scalar-distributive scalar-associative
scalar-unital
proof
let X be RealNormSpace;
set RBLOP=R_Normed_Algebra_of_BoundedLinearOperators(X);
set BS=R_NormSpace_of_BoundedLinearOperators(X,X);
set ADD=Add_(BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X
,X));
set EXMULT =Mult_(BoundedLinearOperators(X,X),
R_VectorSpace_of_LinearOperators(X,X));
set NRM=BoundedLinearOperatorsNorm(X,X);
A1: ||.0.BS.|| = NRM.(0.BS)
.= ||.0.RBLOP.||;
thus ||.0.RBLOP.|| = 0 by A1;
A2: now
let x,y be Point of RBLOP;
let a be Real;
reconsider x1 =x, y1 =y as Point of BS;
A3: ||.x1.|| + ||. y1.|| = NRM.(x1) + ||. y1.||
.= NRM.(x1) + NRM.(y1)
.= ||.x.|| +( the normF of RBLOP ).y
.= ||.x.|| + ||.y.||;
||.x + y.|| = NRM.(ADD.(x,y))
.= ||.x1 + y1.||;
hence ||.x + y.|| <= ||.x.|| + ||. y.|| by A3,NORMSP_1:def 1;
A4: ||.x1.|| = NRM.(x1)
.= ||.x.||;
0.BS=0.RBLOP;
hence ||.x.|| = 0 iff x= 0.RBLOP by A4,NORMSP_0:def 5;
thus ||.a*x.|| = NRM.(EXMULT.(a,x))
.= ||.a*x1.||
.=|.a.|* ||.x.|| by A4,NORMSP_1:def 1;
end;
A5: RBLOP is right_complementable
proof
let x be Element of RBLOP;
thus ex t being Element of RBLOP st x+t= 0.RBLOP by Th19;
end;
( for x,y,z being Element of R_Normed_Algebra_of_BoundedLinearOperators(
X) for a,b be Real holds x+y = y+x & (x+y)+z = x+(y+z) & x+(0.
R_Normed_Algebra_of_BoundedLinearOperators(X)) = x & (ex t being Element of
R_Normed_Algebra_of_BoundedLinearOperators(X) st x+t= 0.
R_Normed_Algebra_of_BoundedLinearOperators(X)) & (x*y)*z = x*(y*z) & x*(1.
R_Normed_Algebra_of_BoundedLinearOperators(X)) = x & (1.
R_Normed_Algebra_of_BoundedLinearOperators(X))*x = x & x*(y+z) = x*y + x*z & (y
+z)*x = y*x + z*x & a*(x*y) = (a*x)*y & (a*b)*(x*y)=(a*x)*(b*y) & a*(x+y) = a*x
+ a*y & (a+b)*x = a*x + b*x & (a*b)*x = a*(b*x) & 1*x=x)& for a be Real
for v,w being VECTOR of RBLOP holds a * (v + w) = a * v + a * w by Th19;
hence thesis by A5,A2,NORMSP_1:def 1;
end;
registration
cluster reflexive discerning RealNormSpace-like Abelian add-associative
right_zeroed
right_complementable associative right_unital right-distributive
vector-distributive scalar-distributive scalar-associative vector-associative
vector-distributive scalar-distributive scalar-associative
scalar-unital strict for non empty Normed_AlgebraStr;
existence
proof
set X = the RealNormSpace;
take R_Normed_Algebra_of_BoundedLinearOperators(X);
thus thesis by Th20;
end;
end;
definition
mode Normed_Algebra is reflexive discerning RealNormSpace-like
Abelian add-associative right_zeroed right_complementable associative
right_unital right-distributive
vector-distributive scalar-distributive scalar-associative
vector-associative scalar-unital non empty Normed_AlgebraStr;
end;
registration
let X be RealNormSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators(X) ->
reflexive discerning RealNormSpace-like
Abelian add-associative right_zeroed right_complementable associative
right_unital right-distributive vector-distributive scalar-distributive
scalar-associative vector-associative scalar-unital;
correctness by Th20;
end;
definition
let X be non empty Normed_AlgebraStr;
attr X is Banach_Algebra-like_1 means
for x,y being Element of X holds ||. x *y .|| <= ||.x.|| * ||.y.||;
attr X is Banach_Algebra-like_2 means
||. 1.X .|| = 1;
attr X is Banach_Algebra-like_3 means
for a being Real for x,y being Element of X holds a*(x*y)=x*(a*y);
end;
definition
let X be Normed_Algebra;
attr X is Banach_Algebra-like means
X is Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
left_unital left-distributive complete;
end;
registration
cluster Banach_Algebra-like -> Banach_Algebra-like_1 Banach_Algebra-like_2
Banach_Algebra-like_3 left-distributive left_unital complete for
Normed_Algebra;
coherence;
cluster Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
left-distributive left_unital complete -> Banach_Algebra-like for
Normed_Algebra;
coherence;
end;
registration
let X be non trivial RealBanachSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators(X) -> Banach_Algebra-like;
coherence
proof
set NRM=BoundedLinearOperatorsNorm(X,X);
set UNIT=FuncUnit(X);
set MULT= FuncMult(X);
set ADD=Add_(BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators
(X,X));
set BS=R_NormSpace_of_BoundedLinearOperators(X,X);
set BLOP=BoundedLinearOperators(X,X);
set RBLOP=R_Normed_Algebra_of_BoundedLinearOperators(X);
thus RBLOP is Banach_Algebra-like_1
proof
let x,y be Point of RBLOP;
reconsider x1=x,y1=y as Element of BLOP;
A1: NRM.(modetrans(x1,X,X)) *NRM.(modetrans(y1,X,X)) =NRM.(x1)*NRM.(
modetrans(y1,X,X)) by LOPBAN_1:def 11
.=NRM.(x1) *NRM.(y1) by LOPBAN_1:def 11
.= ||.x .|| * NRM.(y)
.= ||.x .|| * ||.y .||;
||.x * y.|| = NRM.(MULT.(x,y))
.= NRM.(x1*y1) by Def4
.= NRM.(modetrans(x1,X,X)*modetrans(y1,X,X));
hence thesis by A1,Th2;
end;
||. 1.RBLOP .|| = NRM.(id (the carrier of X))
.= 1 by Th18;
hence RBLOP is Banach_Algebra-like_2;
thus RBLOP is Banach_Algebra-like_3
proof
let a be Real;
let x,y be Element of RBLOP;
thus a*(x*y)=(1*a)*(x*y) .=(1*x)*(a*y) by Th19
.=x*(a*y) by Th19;
end;
thus RBLOP is left_unital
proof
let x be Element of RBLOP;
reconsider xx=x as Element of BLOP;
UNIT*xx = xx by Th8;
hence thesis by Def4;
end;
thus RBLOP is left-distributive
proof
let x,y,z be Element of RBLOP;
reconsider xx=x,yy=y,zz=z as Element of BLOP;
thus (y+z)*x = (yy+zz)*xx by Def4
.= yy*xx + zz*xx by Th10
.= ADD.(yy*xx,MULT.(zz,xx)) by Def4
.= y*x + z*x by Def4;
end;
now
let seq be sequence of RBLOP such that
A2: seq is Cauchy_sequence_by_Norm;
reconsider seq1=seq as sequence of BS;
now
let r be Real;
assume r > 0;
then consider k be Nat such that
A3: for n, m be Nat st n >= k & m >= k holds ||.(seq.n)
- (seq.m).|| < r by A2,RSSPACE3:8;
now
let n, m be Nat such that
A4: n >= k & m >= k;
||.(seq1.n) - (seq1.m).|| = NRM.((seq1.n) +(- (seq1.m)))
.= NRM. (ADD.(seq1.n,(-1)*(seq1.m))) by RLVECT_1:16
.= NRM. (ADD.(seq.n,(-1)*(seq.m)))
.= NRM.((seq.n) +(- (seq.m))) by RLVECT_1:16
.= ||.(seq.n) - (seq.m).||;
hence ||.(seq1.n) - (seq1.m).|| < r by A3,A4;
end;
hence ex k be Nat st for n, m be Nat st n >= k &
m >= k holds ||.(seq1.n) - (seq1.m).|| < r;
end;
then seq1 is Cauchy_sequence_by_Norm by RSSPACE3:8;
then seq1 is convergent by LOPBAN_1:def 15;
then consider g1 be Point of BS such that
A5: for r be Real st 0 < r ex m be Nat st for n be
Nat st m <= n holds ||.(seq1.n) - g1.|| < r by NORMSP_1:def 6;
reconsider g=g1 as Point of RBLOP;
now
let r be Real;
assume 0 < r;
then consider m be Nat such that
A6: for n be Nat st m <= n holds ||.(seq1.n) - g1.|| < r by A5;
now
let n be Nat such that
A7: m <= n;
||.(seq1.n) - (g1).|| = NRM.((seq1.n) +(- (g1)))
.= NRM. (ADD.(seq1.n,(-1)*(g1))) by RLVECT_1:16
.= NRM. (ADD.(seq.n,(-1)*(g)))
.= NRM.((seq.n) +(- (g))) by RLVECT_1:16
.= ||.(seq.n) - (g).||;
hence ||.(seq.n) - (g).|| < r by A6,A7;
end;
hence
ex m be Nat st for n be Nat st m <= n holds
||.(seq.n) - g.|| < r;
end;
hence seq is convergent by NORMSP_1:def 6;
end;
hence thesis;
end;
end;
registration
cluster Banach_Algebra-like for Normed_Algebra;
existence
proof
set X = the non trivial RealBanachSpace;
take R_Normed_Algebra_of_BoundedLinearOperators(X);
thus thesis;
end;
end;
definition
mode Banach_Algebra is Banach_Algebra-like Normed_Algebra;
end;
theorem
for X being RealNormSpace holds 1.Ring_of_BoundedLinearOperators(X) =
FuncUnit(X);
theorem
for X being RealNormSpace holds 1.R_Algebra_of_BoundedLinearOperators(
X) = FuncUnit(X);
theorem
for X being RealNormSpace holds 1.
R_Normed_Algebra_of_BoundedLinearOperators(X) = FuncUnit(X);