:: Banach Algebra of Bounded Complex Linear Operators :: by Noboru Endou :: :: Received March 18, 2004 :: Copyright (c) 2004-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, 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; begin :: Banach Algebra of Bounded Complex Linear Operators theorem :: CLOPBAN2:1 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; theorem :: CLOPBAN2:2 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); definition let X be ComplexNormSpace; let f,g be Lipschitzian LinearOperator of X,X; redefine func g*f -> Lipschitzian LinearOperator of X,X; end; definition let X be ComplexNormSpace; let f,g be Element of BoundedLinearOperators(X,X); func f + g -> Element of BoundedLinearOperators(X,X) equals :: CLOPBAN2:def 1 Add_ ( BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X) ) .(f,g); end; definition let X be ComplexNormSpace; let f,g be Element of BoundedLinearOperators(X,X); func g*f -> Element of BoundedLinearOperators(X,X) equals :: CLOPBAN2:def 2 modetrans(g,X,X)* modetrans(f,X,X); 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 :: CLOPBAN2:def 3 Mult_( BoundedLinearOperators(X,X), C_VectorSpace_of_LinearOperators(X,X)).(z,f); end; definition let X be ComplexNormSpace; func FuncMult(X) -> BinOp of BoundedLinearOperators(X,X) means :: CLOPBAN2:def 4 for f, g being Element of BoundedLinearOperators(X,X) holds it.(f,g) = f*g; end; theorem :: CLOPBAN2:3 for X be ComplexNormSpace holds id (the carrier of X) is Lipschitzian LinearOperator of X,X; definition let X be ComplexNormSpace; func FuncUnit(X) -> Element of BoundedLinearOperators(X,X) equals :: CLOPBAN2:def 5 id (the carrier of X); end; theorem :: CLOPBAN2:4 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); theorem :: CLOPBAN2:5 for X be ComplexNormSpace for f,g,h be Lipschitzian LinearOperator of X,X holds f*(g*h) =(f*g)*h; theorem :: CLOPBAN2:6 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; theorem :: CLOPBAN2:7 for X be ComplexNormSpace for f,g,h be Element of BoundedLinearOperators(X,X) holds f*(g*h) =(f*g)*h; theorem :: CLOPBAN2:8 for X be ComplexNormSpace for f be Element of BoundedLinearOperators(X,X) holds f*FuncUnit(X)= f & FuncUnit(X)*f=f; theorem :: CLOPBAN2:9 for X be ComplexNormSpace for f,g,h be Element of BoundedLinearOperators(X,X) holds f *(g+h)=f*g + f*h; theorem :: CLOPBAN2:10 for X be ComplexNormSpace for f,g,h be Element of BoundedLinearOperators(X,X) holds (g+h)*f = g*f + h*f; theorem :: CLOPBAN2:11 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); theorem :: CLOPBAN2:12 for X be ComplexNormSpace for f,g be Element of BoundedLinearOperators(X,X) for a be Complex holds a*(f*g) =(a*f)*g; definition let X be ComplexNormSpace; func Ring_of_BoundedLinearOperators(X) -> doubleLoopStr equals :: CLOPBAN2:def 6 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)) #); end; registration let X be ComplexNormSpace; cluster Ring_of_BoundedLinearOperators(X) -> non empty strict; end; registration let X be ComplexNormSpace; cluster Ring_of_BoundedLinearOperators(X) -> unital; end; theorem :: CLOPBAN2:13 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; theorem :: CLOPBAN2:14 for X be ComplexNormSpace holds Ring_of_BoundedLinearOperators(X) is Ring; registration let X be ComplexNormSpace; cluster Ring_of_BoundedLinearOperators(X) -> Abelian add-associative right_zeroed right_complementable associative well-unital distributive; end; definition let X be ComplexNormSpace; func C_Algebra_of_BoundedLinearOperators(X) -> ComplexAlgebraStr equals :: CLOPBAN2:def 7 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)) #) ; end; registration let X be ComplexNormSpace; cluster C_Algebra_of_BoundedLinearOperators(X) -> non empty strict; end; registration let X be ComplexNormSpace; cluster C_Algebra_of_BoundedLinearOperators(X) -> unital; end; theorem :: CLOPBAN2:15 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); 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; end; theorem :: CLOPBAN2:16 for X be ComplexNormSpace holds C_Algebra_of_BoundedLinearOperators(X) is ComplexBLAlgebra; registration cluster Complex_l1_Space -> complete; end; registration cluster Complex_l1_Space -> non trivial; end; registration cluster non trivial for ComplexBanachSpace; end; theorem :: CLOPBAN2:17 for X be non trivial ComplexNormSpace ex w be VECTOR of X st ||. w .|| = 1; theorem :: CLOPBAN2:18 for X be non trivial ComplexNormSpace holds BoundedLinearOperatorsNorm(X,X).(id the carrier of X) = 1; 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; end; definition let X be ComplexNormSpace; func C_Normed_Algebra_of_BoundedLinearOperators(X) -> Normed_Complex_AlgebraStr equals :: CLOPBAN2:def 8 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) #); end; registration let X be ComplexNormSpace; cluster C_Normed_Algebra_of_BoundedLinearOperators(X) -> non empty strict; end; registration let X be ComplexNormSpace; cluster C_Normed_Algebra_of_BoundedLinearOperators(X) -> unital; end; theorem :: CLOPBAN2:19 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; theorem :: CLOPBAN2:20 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; 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; 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; end; definition let X be non empty Normed_Complex_AlgebraStr; attr X is Banach_Algebra-like_1 means :: CLOPBAN2:def 9 for x,y being Element of X holds ||. x*y .|| <= ||.x.|| * ||.y.||; attr X is Banach_Algebra-like_2 means :: CLOPBAN2:def 10 ||. 1.X .|| = 1; attr X is Banach_Algebra-like_3 means :: CLOPBAN2:def 11 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 :: CLOPBAN2:def 12 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; 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; end; registration let X be non trivial ComplexBanachSpace; cluster C_Normed_Algebra_of_BoundedLinearOperators(X) -> Banach_Algebra-like; end; registration cluster Banach_Algebra-like for Normed_Complex_Algebra; end; definition mode Complex_Banach_Algebra is Banach_Algebra-like Normed_Complex_Algebra; end; theorem :: CLOPBAN2:21 for X being ComplexNormSpace holds 1.Ring_of_BoundedLinearOperators(X) = FuncUnit(X); theorem :: CLOPBAN2:22 for X being ComplexNormSpace holds 1. C_Algebra_of_BoundedLinearOperators(X) = FuncUnit(X); theorem :: CLOPBAN2:23 for X being ComplexNormSpace holds 1. C_Normed_Algebra_of_BoundedLinearOperators(X) = FuncUnit(X);