:: Banach Algebra of Bounded Complex Linear Operators
:: by Noboru Endou
::
:: Received March 18, 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, CLVECT_1, LOPBAN_1, RELAT_1, RLVECT_1, FUNCT_1, ARYTM_3,
XXREAL_2, NORMSP_1, XXREAL_0, PRE_TOPC, CLOPBAN1, CARD_1, REAL_1,
SUBSET_1, RSSPACE, LOPBAN_2, BINOP_1, STRUCT_0, COMPLEX1, ALGSTR_0,
XBOOLE_0, GROUP_1, SUPINF_2, MESFUNC1, FUNCSDOM, VECTSP_1, LATTICES,
CFUNCDOM, CSSPACE3, REWRITE1, NAT_1, RSSPACE3, SEQ_2, ZFMISC_1, XCMPLX_0,
PREPOWER, COMSEQ_1, SERIES_1, CSSPACE, ARYTM_1, CLOPBAN2, NORMSP_0,
METRIC_1, RELAT_2, SEQ_4, FCONT_1;
notations XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, PARTFUN1, FUNCT_2, PRE_TOPC,
BINOP_1, STRUCT_0, ALGSTR_0, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1,
NUMBERS, XXREAL_2, REAL_1, RLVECT_1, VALUED_1, SEQ_4, COMPLEX1, GROUP_1,
VECTSP_1, SERIES_1, COMSEQ_1, COMSEQ_3, NORMSP_0, CLVECT_1, CSSPACE,
CSSPACE3, CLOPBAN1, CFUNCDOM, PREPOWER;
constructors REAL_1, PREPOWER, COMSEQ_3, CSSPACE3, CLOPBAN1, CFUNCDOM,
VECTSP_1, SEQ_4, RELSET_1, BINOP_2, BINOP_1, GROUP_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, CLVECT_1, CSSPACE3,
CLOPBAN1, CFUNCDOM, ALGSTR_0, VALUED_1, VALUED_0, NORMSP_0;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions STRUCT_0, GROUP_1, VECTSP_1, RLVECT_1, ALGSTR_0, CLVECT_1,
CFUNCDOM, NORMSP_0;
equalities STRUCT_0, CLOPBAN1, BINOP_1, ALGSTR_0, CLVECT_1, NORMSP_0;
expansions STRUCT_0, GROUP_1, VECTSP_1, CLOPBAN1, BINOP_1, RLVECT_1, ALGSTR_0,
CLVECT_1, CFUNCDOM;
theorems ABSVALUE, RLVECT_1, VECTSP_1, XCMPLX_0, SERIES_1, FUNCT_2, SEQ_4,
PREPOWER, STRUCT_0, CLOPBAN1, CLVECT_1, COMPLEX1, CSSPACE3, COMSEQ_3,
CSSPACE, GROUP_1, XREAL_1, XXREAL_0, ALGSTR_0, VALUED_1, NORMSP_0;
schemes BINOP_1;
begin :: Banach Algebra of Bounded Complex Linear Operators
theorem Th1:
for X,Y,Z be ComplexLinearSpace, f be LinearOperator of X,Y, g be
LinearOperator of Y,Z holds g*f is LinearOperator of X,Z
proof
let X,Y,Z be ComplexLinearSpace;
let f be LinearOperator of X,Y;
let g be LinearOperator of Y,Z;
A1: now
let v be VECTOR of X, z be Complex;
thus (g*f).(z*v) =g.(f.(z*v)) by FUNCT_2:15
.=g.(z*f.v) by CLOPBAN1:def 3
.=z*g.(f.v) by CLOPBAN1:def 3
.=z*(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,CLOPBAN1:def 3,VECTSP_1:def 20;
end;
theorem Th2:
for X,Y,Z be ComplexNormSpace 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 ComplexNormSpace;
let f be Lipschitzian LinearOperator of X,Y;
let g be Lipschitzian LinearOperator of Y,Z;
reconsider ff=f as Point of C_NormSpace_of_BoundedLinearOperators(X,Y) by
CLOPBAN1:def 7;
reconsider gg=g as Point of C_NormSpace_of_BoundedLinearOperators(Y,Z) by
CLOPBAN1:def 7;
A1: now
let v be VECTOR of X;
0 <= ||.gg.|| by CLVECT_1:105;
then
A2: ||.gg.||*||.f.(v).|| <=||.gg.||*(||.ff.||*||.v.||) by CLOPBAN1:31
,XREAL_1:64;
||.(g*f).v.|| = ||.g.(f.v).|| & ||.g.(f.(v)).|| <=||.gg.|| * ||.f.(v)
.|| by CLOPBAN1:31,FUNCT_2:15;
hence ||.(g*f).v.|| <=(||.gg.|| * ||.ff.||) * ||.v.|| by A2,XXREAL_0:2;
end;
set K = ||.gg.|| * ||.ff.||;
A3: 0 <= ||.gg.|| & 0 <= ||.ff.|| by CLVECT_1:105;
then reconsider gf=g*f as Lipschitzian LinearOperator of X,Z by A1,Th1,
CLOPBAN1:def 6;
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,CLOPBAN1:29;
end;
definition
let X be ComplexNormSpace;
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 ComplexNormSpace;
let f,g be Element of BoundedLinearOperators(X,X);
func f + g -> Element of BoundedLinearOperators(X,X) equals
Add_ (
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X) ) .(f,g);
correctness;
end;
definition
let X be ComplexNormSpace;
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 CLOPBAN1:def 7;
end;
definition
let X be ComplexNormSpace;
let f be Element of BoundedLinearOperators(X,X);
let z be Complex;
func z*f -> Element of BoundedLinearOperators(X,X) equals
Mult_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)).(z,f);
correctness
proof
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
Mult_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)).(z,f)
is Element of BoundedLinearOperators(X,X);
hence thesis;
end;
end;
definition
let X be ComplexNormSpace;
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;
end;
end;
theorem Th3:
for X be ComplexNormSpace holds id (the carrier of X) is Lipschitzian
LinearOperator of X,X
proof
let X be ComplexNormSpace;
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, z be Complex
holds (id the carrier of X).(z*v) = z*(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,CLOPBAN1:def 3,def 6,VECTSP_1:def 20;
end;
definition
let X be ComplexNormSpace;
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 CLOPBAN1:def 7;
end;
end;
theorem Th4:
for X be ComplexNormSpace 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 ComplexNormSpace;
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 ComplexNormSpace for f,g,h be Lipschitzian LinearOperator of
X,X holds f*(g*h) =(f*g)*h
proof
let X be ComplexNormSpace;
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 ComplexNormSpace 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 ComplexNormSpace;
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 ComplexNormSpace for f,g,h be Element of
BoundedLinearOperators(X,X) holds f*(g*h) =(f*g)*h
proof
let X be ComplexNormSpace;
let f,g,h be Element of BoundedLinearOperators(X,X);
modetrans((g*h),X,X) =modetrans(g,X,X)*modetrans(h,X,X) by CLOPBAN1:def 9;
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 CLOPBAN1:def 9;
end;
theorem Th8:
for X be ComplexNormSpace for f be Element of
BoundedLinearOperators(X,X) holds f*FuncUnit(X)= f & FuncUnit(X)*f=f
proof
let X be ComplexNormSpace;
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
CLOPBAN1:def 7;
then
A1: modetrans( (id (the carrier of X)),X,X) = (id the carrier of X) by
CLOPBAN1:def 9;
hence f*FuncUnit(X) =modetrans(f,X,X) by Th6
.=f by CLOPBAN1:def 9;
thus FuncUnit(X)*f =modetrans(f,X,X) by A1,Th6
.=f by CLOPBAN1:def 9;
end;
theorem Th9:
for X be ComplexNormSpace for f,g,h be Element of
BoundedLinearOperators(X,X) holds f *(g+h)=f*g + f*h
proof
let X be ComplexNormSpace;
let f,g,h be Element of BoundedLinearOperators(X,X);
set BLOP=C_NormSpace_of_BoundedLinearOperators(X,X);
set ADD=Add_(BoundedLinearOperators(X,X), C_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 CLOPBAN1:def 7;
reconsider fg=mf*mg as VECTOR of BLOP by CLOPBAN1:def 7;
reconsider k=mf*mgh as VECTOR of BLOP by CLOPBAN1:def 7;
reconsider hh = h as VECTOR of BLOP;
reconsider gg = g as VECTOR of BLOP;
A1: gg=mg & hh=mh by CLOPBAN1:def 9;
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 CLOPBAN1:def 9;
then
A2: mgh.x=mg.x+mh.x by A1,CLOPBAN1:34;
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 CLOPBAN1:34;
hence thesis;
end;
hence thesis;
end;
theorem Th10:
for X be ComplexNormSpace for f,g,h be Element of
BoundedLinearOperators(X,X) holds (g+h)*f = g*f + h*f
proof
let X be ComplexNormSpace;
let f,g,h be Element of BoundedLinearOperators(X,X);
set BLOP=C_NormSpace_of_BoundedLinearOperators(X,X);
set ADD=Add_(BoundedLinearOperators(X,X), C_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 CLOPBAN1:def 7;
reconsider gf=mg*mf as VECTOR of BLOP by CLOPBAN1:def 7;
reconsider k=mgh*mf as VECTOR of BLOP by CLOPBAN1:def 7;
reconsider hh = h as VECTOR of BLOP;
reconsider gg = g as VECTOR of BLOP;
A1: gg=mg & hh=mh by CLOPBAN1:def 9;
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 CLOPBAN1:def 9;
then
A2: mgh.(mf.x)=mg.(mf.x)+mh.(mf.x) by A1,CLOPBAN1:34;
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 CLOPBAN1:34;
hence thesis;
end;
hence thesis;
end;
theorem Th11:
for X be ComplexNormSpace for f,g be Element of
BoundedLinearOperators(X,X) for a,b be Complex holds (a*b)*(f*g)=(a*f)*(b*g)
proof
let X be ComplexNormSpace;
let f,g be Element of BoundedLinearOperators(X,X);
let a,b be Complex;
set BLOP=C_NormSpace_of_BoundedLinearOperators(X,X);
set EXMULT=Mult_(BoundedLinearOperators(X,X),
C_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 CLOPBAN1:def 7;
reconsider fg=mf*mg as VECTOR of BLOP by CLOPBAN1:def 7;
reconsider ff = f, gg = g as VECTOR of BLOP;
A1: gg=mg by CLOPBAN1:def 9;
A2: ff=mf by CLOPBAN1:def 9;
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 CLOPBAN1:def 9;
then
A3: maf.y=a*mf.y by A2,CLOPBAN1:35;
b*g=b*gg & modetrans(b*g, X,X) =b*g by CLOPBAN1:def 9;
then
A4: mbg.x=b*mg.x by A1,CLOPBAN1:35;
thus (maf*mbg).x=maf.(mbg.x) by Th4
.=a*(b*mf.(mg.x)) by A3,A4,CLOPBAN1:def 3
.=(a*b)*mf.(mg.x) by CLVECT_1:def 4
.=(a*b)*(mf*mg).x by Th4;
end;
then k=(a*b)*fg by CLOPBAN1:35;
hence thesis;
end;
hence thesis;
end;
theorem Th12:
for X be ComplexNormSpace for f,g be Element of
BoundedLinearOperators(X,X) for a be Complex holds a*(f*g) =(a*f)*g
proof
let X be ComplexNormSpace;
let f,g be Element of BoundedLinearOperators(X,X);
let a be Complex;
set RRL=CLSStruct (# BoundedLinearOperators(X,X), Zero_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), Add_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)) #);
reconsider gg=g as Element of RRL;
A1: (1r*g)=1r*gg .=g by CLVECT_1:def 5;
a*(f*g)=(a*1r)*(f*g) by COMPLEX1:def 4
.=(a*f)*(1r*g) by Th11;
hence thesis by A1;
end;
definition
let X be ComplexNormSpace;
func Ring_of_BoundedLinearOperators(X) -> doubleLoopStr equals
doubleLoopStr
(# BoundedLinearOperators(X,X), Add_(BoundedLinearOperators(X,X),
C_VectorSpace_of_LinearOperators(X,X)), FuncMult(X), FuncUnit(X), Zero_(
BoundedLinearOperators(X,X),C_VectorSpace_of_LinearOperators(X,X)) #);
correctness;
end;
registration
let X be ComplexNormSpace;
cluster Ring_of_BoundedLinearOperators(X) -> non empty strict;
coherence;
end;
Lm1: now
let X be ComplexNormSpace;
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 ComplexNormSpace;
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 ComplexNormSpace 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 & x is right_complementable & (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 ComplexNormSpace;
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), C_VectorSpace_of_LinearOperators(X
,X));
set MULT= FuncMult(X);
set UNIT=FuncUnit(X);
set RRL=CLSStruct (# BoundedLinearOperators(X,X), Zero_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), Add_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), C_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 by RLVECT_1:def 4;
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 ComplexNormSpace holds Ring_of_BoundedLinearOperators(X) is Ring
proof
let X be ComplexNormSpace;
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 & x is
right_complementable & (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 ALGSTR_0:def 16,GROUP_1:def 3,RLVECT_1:def 2,def 3,def 4
,VECTSP_1:def 6,def 7;
end;
registration
let X be ComplexNormSpace;
cluster Ring_of_BoundedLinearOperators(X) -> Abelian add-associative
right_zeroed right_complementable associative well-unital distributive;
coherence by Th14;
end;
definition
let X be ComplexNormSpace;
func C_Algebra_of_BoundedLinearOperators(X) -> ComplexAlgebraStr equals
ComplexAlgebraStr (# BoundedLinearOperators(X,X), FuncMult(X), Add_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), FuncUnit(X
), Zero_(BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)) #)
;
correctness;
end;
registration
let X be ComplexNormSpace;
cluster C_Algebra_of_BoundedLinearOperators(X) -> non empty strict;
coherence;
end;
Lm2: now
let X be ComplexNormSpace;
set F = C_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 ComplexNormSpace;
cluster C_Algebra_of_BoundedLinearOperators(X) -> unital;
coherence
proof
reconsider e = FuncUnit(X) as Element of
C_Algebra_of_BoundedLinearOperators(X);
take e;
thus thesis by Lm2;
end;
end;
theorem
for X be ComplexNormSpace for x,y,z being Element of
C_Algebra_of_BoundedLinearOperators(X) for a,b be Complex holds x+y = y+x & (x+
y)+z = x+(y+z) & x+(0.C_Algebra_of_BoundedLinearOperators(X)) = x & x is
right_complementable & (x*y)*z = x*(y*z) & x*(1.
C_Algebra_of_BoundedLinearOperators(X)) = x & (1.
C_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 ComplexNormSpace;
let x,y,z be Element of C_Algebra_of_BoundedLinearOperators(X);
let a,b be Complex;
set RBLOP=C_Algebra_of_BoundedLinearOperators(X);
set BLOP=BoundedLinearOperators(X,X);
set ADD=Add_(BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X
,X));
set MULT= FuncMult(X);
set UNIT=FuncUnit(X);
set RRL=CLSStruct (# BoundedLinearOperators(X,X), Zero_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), Add_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), C_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 by RLVECT_1:def 4;
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 CLVECT_1:def 2
.=a*x+a*y;
thus (a+b)*x =(a+b)*f .=a*f+b*f by CLVECT_1:def 3
.=a*x+b*x;
thus (a*b)*x =(a*b)*f .=a*(b*f) by CLVECT_1:def 4
.=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 ComplexBLAlgebra is Abelian add-associative right_zeroed
right_complementable associative right_unital right-distributive
vector-distributive scalar-distributive scalar-associative
vector-associative non empty ComplexAlgebraStr;
end;
registration let X be ComplexNormSpace;
cluster C_Algebra_of_BoundedLinearOperators X ->
Abelian add-associative right_zeroed
right_complementable associative right_unital right-distributive
vector-distributive scalar-distributive scalar-associative
vector-associative;
coherence
proof set A = C_Algebra_of_BoundedLinearOperators X;
set MULT= FuncMult(X);
set UNIT=FuncUnit(X);
set BLOP=BoundedLinearOperators(X,X);
set ADD=Add_(BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X
,X));
set RRL=CLSStruct (# BoundedLinearOperators(X,X), Zero_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), Add_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), C_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 by RLVECT_1:def 4;
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 Complex; 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 CLVECT_1:def 2
.=a*x+a*y;
end;
thus A is scalar-distributive
proof let a,b be Complex; 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 CLVECT_1:def 3
.=a*x+b*x;
end;
thus A is scalar-associative
proof let a,b be Complex; let x be Element of A;
reconsider f=x as Element of RRL;
thus (a*b)*x =(a*b)*f .=a*(b*f) by CLVECT_1:def 4
.=a*(b*x);
end;
let x,y be Element of A; let a be Complex;
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;
end;
theorem
for X be ComplexNormSpace holds C_Algebra_of_BoundedLinearOperators(X)
is ComplexBLAlgebra;
registration
cluster Complex_l1_Space -> complete;
coherence
by CSSPACE3:9;
end;
registration
cluster Complex_l1_Space -> non trivial;
coherence
proof
reconsider a=1/2+0*<i> as Element of COMPLEX by XCMPLX_0:def 2;
reconsider x = a GeoSeq as Complex_Sequence;
A1: for m be Nat holds (|.x.|).(m+1) = (|.x.|).m * |.a.|
proof
let m be Nat;
(|.x.|).(m+1) = |. x.(m+1) .| by VALUED_1:18
.= |. x.m * a .| by COMSEQ_3:def 1
.= |. x.m .| * |.a.| by COMPLEX1:65;
hence thesis by VALUED_1:18;
end;
(|.x.|).0 = |. x.0 .| by VALUED_1:18
.= 1 by COMPLEX1:48,COMSEQ_3:def 1;
then |.a.| = 1/2 & |.x.| = |.a.| GeoSeq by A1,ABSVALUE:def 1,PREPOWER:3;
then |.x.| is summable by SERIES_1:24;
then x is absolutely_summable by COMSEQ_3:def 9;
then seq_id(x) is absolutely_summable by CSSPACE:1;
then reconsider v=x as VECTOR of Complex_l1_Space by CSSPACE3:6;
(seq_id v).0 = x.0 by CSSPACE:1
.= 1 by COMPLEX1:def 4,COMSEQ_3:def 1;
then v <> CZeroseq by CSSPACE:4;
hence thesis by CSSPACE3:6;
end;
end;
registration
cluster non trivial for ComplexBanachSpace;
existence
proof
take Complex_l1_Space;
thus thesis;
end;
end;
theorem Th17:
for X be non trivial ComplexNormSpace ex w be VECTOR of X st ||. w .|| = 1
proof
let X be non trivial ComplexNormSpace;
consider v be VECTOR of X such that
A1: v <> 0.X by STRUCT_0:def 18;
reconsider a= ||. v .||+0*<i> as Element of COMPLEX by XCMPLX_0:def 2;
take w=a"*v;
A2: ||. v .|| <> 0 by A1,NORMSP_0:def 5;
then
A3: 0 < ||. v .|| by CLVECT_1:105;
A4: |.a".| = |.(1r*a").| by COMPLEX1:def 4
.= |.1r/a.| by XCMPLX_0:def 9
.= 1/|.a.| by COMPLEX1:48,67
.= 1*|.a.|" by XCMPLX_0:def 9
.= ||.v.||"by A3,ABSVALUE:def 1;
thus ||.w.|| =|.a".|*||.v.|| by CLVECT_1:def 13
.=1 by A2,A4,XCMPLX_0:def 7;
end;
theorem Th18:
for X be non trivial ComplexNormSpace holds
BoundedLinearOperatorsNorm(X,X).(id the carrier of X) = 1
proof
let X be non trivial ComplexNormSpace;
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 CLOPBAN1:26;
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 CLOPBAN1:29;
end;
definition
struct(ComplexAlgebraStr,CNORMSTR) Normed_Complex_AlgebraStr (# carrier ->
set, multF,addF -> (BinOp of the carrier), Mult -> (Function of [:COMPLEX,the
carrier:],the carrier), OneF,ZeroF -> Element of the carrier, normF -> Function
of the carrier, REAL#);
end;
registration
cluster non empty for Normed_Complex_AlgebraStr;
existence
proof
set A = the non empty set,m = the BinOp of A,a = the BinOp of A,M =the
Function of [:COMPLEX,A:],A,U = the Element of A,Z = the Element of A,n =the
Function of A,REAL;
take Normed_Complex_AlgebraStr(#A,m,a,M,U,Z,n#);
thus the carrier of Normed_Complex_AlgebraStr(#A,m,a,M,U,Z,n#) is non
empty;
end;
end;
definition
let X be ComplexNormSpace;
func C_Normed_Algebra_of_BoundedLinearOperators(X) ->
Normed_Complex_AlgebraStr equals
Normed_Complex_AlgebraStr (#
BoundedLinearOperators(X,X), FuncMult(X), Add_(BoundedLinearOperators(X,X),
C_VectorSpace_of_LinearOperators(X,X)), Mult_(BoundedLinearOperators(X,X),
C_VectorSpace_of_LinearOperators(X,X)), FuncUnit(X), Zero_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)),
BoundedLinearOperatorsNorm(X,X) #);
correctness;
end;
registration
let X be ComplexNormSpace;
cluster C_Normed_Algebra_of_BoundedLinearOperators(X) -> non empty strict;
coherence;
end;
Lm3: now
let X be ComplexNormSpace;
set F = C_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 ComplexNormSpace;
cluster C_Normed_Algebra_of_BoundedLinearOperators(X) -> unital;
coherence
proof
reconsider e = FuncUnit(X) as Element of
C_Normed_Algebra_of_BoundedLinearOperators(X);
take e;
thus thesis by Lm3;
end;
end;
theorem Th19:
for X be ComplexNormSpace for x,y,z being Element of
C_Normed_Algebra_of_BoundedLinearOperators(X) for a,b be Complex holds x+y = y+
x & (x+y)+z = x+(y+z) & x+(0.C_Normed_Algebra_of_BoundedLinearOperators(X)) = x
& x is right_complementable & (x*y)*z = x*(y*z) & x*(1.
C_Normed_Algebra_of_BoundedLinearOperators(X)) = x & (1.
C_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) & 1r*x =x
proof
let X be ComplexNormSpace;
let x,y,z be Element of C_Normed_Algebra_of_BoundedLinearOperators(X);
let a,b be Complex;
set RBLOP=C_Normed_Algebra_of_BoundedLinearOperators(X);
set BLOP=BoundedLinearOperators(X,X);
set ADD=Add_(BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X
,X));
set MULT= FuncMult(X);
set UNIT=FuncUnit(X);
set RRL=CLSStruct (# BoundedLinearOperators(X,X), Zero_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), Add_(
BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)), Mult_(
BoundedLinearOperators(X,X), C_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 by RLVECT_1:def 4;
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*b)*(x*y) = (a*b)*(xx*yy) by Def4
.= (a*xx)*(b*yy) by Th11
.=(a*x)*(b*y) by Def4;
thus a*(x+y) =a*(f+g) .=a*f+a*g by CLVECT_1:def 2
.=a*x+a*y;
thus (a+b)*x =(a+b)*f .=a*f+b*f by CLVECT_1:def 3
.=a*x+b*x;
thus (a*b)*x =(a*b)*f .=a*(b*f) by CLVECT_1:def 4
.=a*(b*x);
thus 1r*x =1r*f .=x by CLVECT_1:def 5;
end;
theorem Th20:
for X be ComplexNormSpace holds
C_Normed_Algebra_of_BoundedLinearOperators(X) is
reflexive discerning ComplexNormSpace-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 ComplexNormSpace;
set C = C_Normed_Algebra_of_BoundedLinearOperators X;
set BS=C_NormSpace_of_BoundedLinearOperators(X,X);
thus C is reflexive
proof
thus ||.0.C.|| = ||.0.BS.|| .= 0;
end;
thus C is discerning
proof
let x be Point of C;
reconsider y =x as Point of BS;
assume ||.x.|| = 0;
then ||.y.|| = 0;
then y= 0.BS by NORMSP_0:def 5;
hence x= 0.C;
end;
thus C is ComplexNormSpace-like
proof
let x,y be Point of C;
let a be Complex;
reconsider x1 =x, y1 =y as Point of BS;
A1: ||.x1.|| = ||.x.||;
thus ||.a*x.|| = ||.a*x1.||
.=|.a.|* ||.x.|| by A1,CLVECT_1:def 13;
||.x + y.|| = ||.x1 + y1.|| & ||.x1.|| + ||. y1.|| = ||.x.|| + ||.y.||;
hence thesis by CLVECT_1:def 13;
end;
set RBLOP=C;
(for x,y,z being Element of C for a,b be Complex holds
x+y = y+x & (x+y)+z = x +(y+z) & x+(0.C) = x &
x is right_complementable & (x*y)*z = x*(y*z) &
x*(1.C) = x & (1.C)*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) & 1r*x=x) &
for a be Complex,
v,w being VECTOR of RBLOP holds a * (v + w) = a * v + a * w
by Th19;
hence thesis;
end;
registration
cluster reflexive discerning ComplexNormSpace-like Abelian add-associative
right_zeroed right_complementable associative right_unital
right-distributive vector-distributive scalar-distributive
scalar-associative vector-associative scalar-unital strict for non empty
Normed_Complex_AlgebraStr;
existence
proof
set X = the ComplexNormSpace;
take C_Normed_Algebra_of_BoundedLinearOperators(X);
thus thesis by Th20;
end;
end;
definition
mode Normed_Complex_Algebra is
reflexive discerning ComplexNormSpace-like Abelian add-associative
right_zeroed right_complementable associative right_unital
right-distributive vector-distributive vector-associative
scalar-distributive scalar-associative scalar-unital non empty
Normed_Complex_AlgebraStr;
end;
registration
let X be ComplexNormSpace;
cluster C_Normed_Algebra_of_BoundedLinearOperators(X) ->
reflexive discerning ComplexNormSpace-like Abelian add-associative
right_zeroed right_complementable associative right_unital
right-distributive vector-distributive scalar-associative
vector-associative scalar-distributive scalar-unital;
correctness by Th20;
end;
definition
let X be non empty Normed_Complex_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 Complex for x,y being Element of X holds a*(x*y)=x*(a*y);
end;
definition
let X be Normed_Complex_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_Complex_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_Complex_Algebra;
coherence;
end;
registration
let X be non trivial ComplexBanachSpace;
cluster C_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), C_VectorSpace_of_LinearOperators
(X,X));
set BS=C_NormSpace_of_BoundedLinearOperators(X,X);
set BLOP=BoundedLinearOperators(X,X);
set RBLOP=C_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 CLOPBAN1:def 9
.= ||.x .|| * ||.y .|| by CLOPBAN1:def 9;
||.x * y.|| = NRM.(x1*y1) by Def4
.= NRM.(modetrans(x1,X,X)*modetrans(y1,X,X));
hence thesis by A1,Th2;
end;
||. 1.RBLOP .|| = 1 by Th18;
hence RBLOP is Banach_Algebra-like_2;
thus RBLOP is Banach_Algebra-like_3
proof
let a be Complex;
let x,y be Element of RBLOP;
thus a*(x*y)=(1r*a)*(x*y) by COMPLEX1:def 4
.=(1r*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;
thus (1.RBLOP)*x =UNIT*xx by Def4
.= x by Th8;
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,CSSPACE3:8;
now
let n, m be Nat such that
A4: n >= k & m >= k;
||.(seq1.n) - (seq1.m).|| = NRM. (ADD.(seq1.n,(-1r)*(seq1.m)))
by CLVECT_1:3
.= NRM.((seq.n) +((-1r)*(seq.m)))
.= ||.(seq.n) - (seq.m).|| by CLVECT_1:3;
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 CSSPACE3:8;
then seq1 is convergent by CLOPBAN1:def 13;
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;
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. (ADD.(seq1.n,(-1r)*(g1))) by CLVECT_1:3
.= NRM.((seq.n) +((-1r)*(g)))
.= ||.(seq.n) - (g).|| by CLVECT_1:3;
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;
end;
hence thesis;
end;
end;
registration
cluster Banach_Algebra-like for Normed_Complex_Algebra;
existence
proof
take C_Normed_Algebra_of_BoundedLinearOperators(
the non trivial ComplexBanachSpace);
thus thesis;
end;
end;
definition
mode Complex_Banach_Algebra is Banach_Algebra-like Normed_Complex_Algebra;
end;
theorem
for X being ComplexNormSpace holds 1.Ring_of_BoundedLinearOperators(X)
= FuncUnit(X);
theorem
for X being ComplexNormSpace holds 1.
C_Algebra_of_BoundedLinearOperators(X) = FuncUnit(X);
theorem
for X being ComplexNormSpace holds 1.
C_Normed_Algebra_of_BoundedLinearOperators(X) = FuncUnit(X);