:: The {B}anach Algebra of Bounded Linear Operators
::  by Yasunari Shidama
::
:: Received January 26, 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, 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;


begin :: Banach Algebra of Bounded Linear Operators

theorem :: LOPBAN_2:1
  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;

theorem :: LOPBAN_2:2
  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);

definition
  let X be RealNormSpace;
  let f,g be Lipschitzian LinearOperator of X,X;
  redefine func g*f -> Lipschitzian LinearOperator of X,X;
end;

definition
  let X be RealNormSpace;
  let f,g be Element of BoundedLinearOperators(X,X);
  func f + g -> Element of BoundedLinearOperators(X,X) equals
:: LOPBAN_2:def 1
  Add_ (
  BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X) ) .(f,g);
end;

definition
  let X be RealNormSpace;
  let f,g be Element of BoundedLinearOperators(X,X);
  func g*f -> Element of BoundedLinearOperators(X,X) equals
:: LOPBAN_2:def 2
  modetrans(g,X,X)*modetrans(f,X,X);
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
:: LOPBAN_2:def 3
  Mult_(
  BoundedLinearOperators(X,X), R_VectorSpace_of_LinearOperators(X,X)).(a,f);
end;

definition
  let X be RealNormSpace;
  func FuncMult(X) -> BinOp of BoundedLinearOperators(X,X) means
:: LOPBAN_2:def 4

  for f, g being Element of BoundedLinearOperators(X,X) holds it.(f,g) = f*g;
end;

theorem :: LOPBAN_2:3
  for X be RealNormSpace holds id (the carrier of X) is Lipschitzian
  LinearOperator of X,X;

definition
  let X be RealNormSpace;
  func FuncUnit(X) -> Element of BoundedLinearOperators(X,X) equals
:: LOPBAN_2:def 5
  id (the carrier of X);
end;

theorem :: LOPBAN_2:4
  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);

theorem :: LOPBAN_2:5
  for X be RealNormSpace for f,g,h be Lipschitzian LinearOperator of X,X
  holds f*(g*h) =(f*g)*h;

theorem :: LOPBAN_2:6
  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;

theorem :: LOPBAN_2:7
  for X be RealNormSpace for f,g,h be Element of
  BoundedLinearOperators(X,X) holds f*(g*h) =(f*g)*h;

theorem :: LOPBAN_2:8
  for X be RealNormSpace for f be Element of BoundedLinearOperators
  (X,X) holds f*FuncUnit(X)= f & FuncUnit(X)*f=f;

theorem :: LOPBAN_2:9
  for X be RealNormSpace for f,g,h be Element of
  BoundedLinearOperators(X,X) holds f *(g+h)=f*g + f*h;

theorem :: LOPBAN_2:10
  for X be RealNormSpace for f,g,h be Element of
  BoundedLinearOperators(X,X) holds (g+h)*f = g*f + h*f;

theorem :: LOPBAN_2:11
  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);

theorem :: LOPBAN_2:12
  for X be RealNormSpace for f,g be Element of
  BoundedLinearOperators(X,X) for a be Real holds a*(f*g) =(a*f)*g;

definition
  let X be RealNormSpace;
  func Ring_of_BoundedLinearOperators(X) -> doubleLoopStr equals
:: LOPBAN_2:def 6
  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)) #);
end;

registration
  let X be RealNormSpace;
  cluster Ring_of_BoundedLinearOperators(X) -> non empty strict;
end;

registration
  let X be RealNormSpace;
  cluster Ring_of_BoundedLinearOperators(X) -> unital;
end;

theorem :: LOPBAN_2:13
  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;

theorem :: LOPBAN_2:14
  for X be RealNormSpace holds Ring_of_BoundedLinearOperators(X) is Ring;

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;
end;

definition
  let X be RealNormSpace;
  func R_Algebra_of_BoundedLinearOperators(X) -> AlgebraStr equals
:: LOPBAN_2:def 7
  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)) #);
end;

registration
  let X be RealNormSpace;
  cluster R_Algebra_of_BoundedLinearOperators(X) -> non empty strict;
end;

registration
  let X be RealNormSpace;
  cluster R_Algebra_of_BoundedLinearOperators(X) -> unital;
end;

theorem :: LOPBAN_2:15
  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);

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;
end;

theorem :: LOPBAN_2:16
  for X be RealNormSpace holds R_Algebra_of_BoundedLinearOperators(X) is
  BLAlgebra;

registration
  cluster l1_Space -> complete;
end;

registration
  cluster l1_Space -> non trivial;
end;

registration
  cluster non trivial for RealBanachSpace;
end;

theorem :: LOPBAN_2:17
  for X be non trivial RealNormSpace ex w be VECTOR of X st ||. w .|| = 1;

theorem :: LOPBAN_2:18
  for X be non trivial RealNormSpace holds
  BoundedLinearOperatorsNorm(X,X).(id the carrier of X) = 1;

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;
end;

definition
  let X be RealNormSpace;
  func R_Normed_Algebra_of_BoundedLinearOperators(X) -> Normed_AlgebraStr
  equals
:: LOPBAN_2:def 8
  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) #);
end;

registration
  let X be RealNormSpace;
  cluster R_Normed_Algebra_of_BoundedLinearOperators(X) -> non empty strict;
end;

registration
  let X be RealNormSpace;
  cluster R_Normed_Algebra_of_BoundedLinearOperators(X) -> unital;
end;

theorem :: LOPBAN_2:19
  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;

theorem :: LOPBAN_2:20
  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;

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;
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;
end;

definition
  let X be non empty Normed_AlgebraStr;
  attr X is Banach_Algebra-like_1 means
:: LOPBAN_2:def 9
  for x,y being Element of X holds ||. x *y .|| <= ||.x.|| * ||.y.||;
  attr X is Banach_Algebra-like_2 means
:: LOPBAN_2:def 10
  ||. 1.X .|| = 1;
  attr X is Banach_Algebra-like_3 means
:: LOPBAN_2:def 11
  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
:: LOPBAN_2: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_Algebra;
  cluster Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
left-distributive left_unital complete -> Banach_Algebra-like for
Normed_Algebra;
end;

registration
  let X be non trivial RealBanachSpace;
  cluster R_Normed_Algebra_of_BoundedLinearOperators(X) -> Banach_Algebra-like;
end;

registration
  cluster Banach_Algebra-like for Normed_Algebra;
end;

definition
  mode Banach_Algebra is Banach_Algebra-like Normed_Algebra;
end;

theorem :: LOPBAN_2:21
  for X being RealNormSpace holds 1.Ring_of_BoundedLinearOperators(X) =
  FuncUnit(X);

theorem :: LOPBAN_2:22
  for X being RealNormSpace holds 1.R_Algebra_of_BoundedLinearOperators(
  X) = FuncUnit(X);

theorem :: LOPBAN_2:23
  for X being RealNormSpace holds 1.
  R_Normed_Algebra_of_BoundedLinearOperators(X) = FuncUnit(X);