begin
theorem Th1:
theorem Th2:
for
X,
Y,
Z being
ComplexNormSpace for
f being
bounded LinearOperator of
X,
Y for
g being
bounded LinearOperator of
Y,
Z holds
(
g * f is
bounded LinearOperator of
X,
Z & ( for
x being
VECTOR of 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
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
coherence
(Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) . f,g is Element of BoundedLinearOperators X,X;
;
end;
:: deftheorem defines + CLOPBAN2:def 1 :
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
coherence
(modetrans g,X,X) * (modetrans f,X,X) is Element of BoundedLinearOperators X,X;
by CLOPBAN1:def 8;
end;
:: deftheorem defines * CLOPBAN2:def 2 :
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
coherence
(Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) . z,f is Element of BoundedLinearOperators X,X;
;
end;
:: deftheorem defines * CLOPBAN2:def 3 :
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
ex b1 being BinOp of BoundedLinearOperators X,X st
for f, g being Element of BoundedLinearOperators X,X holds b1 . f,g = f * g
uniqueness
for b1, b2 being BinOp of BoundedLinearOperators X,X st ( for f, g being Element of BoundedLinearOperators X,X holds b1 . f,g = f * g ) & ( for f, g being Element of BoundedLinearOperators X,X holds b2 . f,g = f * g ) holds
b1 = b2
end;
:: deftheorem Def4 defines FuncMult CLOPBAN2:def 4 :
theorem Th3:
:: deftheorem defines FuncUnit CLOPBAN2:def 5 :
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
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
coherence
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)) #) is doubleLoopStr ;
;
end;
:: deftheorem defines Ring_of_BoundedLinearOperators CLOPBAN2:def 6 :
for
X being
ComplexNormSpace holds
Ring_of_BoundedLinearOperators X = 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)) #);
theorem Th13:
theorem Th14:
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
coherence
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)) #) is ComplexAlgebraStr ;
;
end;
:: deftheorem defines C_Algebra_of_BoundedLinearOperators CLOPBAN2:def 7 :
for
X being
ComplexNormSpace holds
C_Algebra_of_BoundedLinearOperators X = 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)) #);
theorem Th15:
theorem
theorem Th17:
theorem Th18:
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
coherence
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) #) is Normed_Complex_AlgebraStr ;
;
end;
:: deftheorem defines C_Normed_Algebra_of_BoundedLinearOperators CLOPBAN2:def 8 :
for
X being
ComplexNormSpace holds
C_Normed_Algebra_of_BoundedLinearOperators X = 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) #);
theorem Th19:
theorem Th20:
:: deftheorem defines Banach_Algebra-like_1 CLOPBAN2:def 9 :
:: deftheorem Def10 defines Banach_Algebra-like_2 CLOPBAN2:def 10 :
:: deftheorem defines Banach_Algebra-like_3 CLOPBAN2:def 11 :
:: deftheorem Def12 defines Banach_Algebra-like CLOPBAN2:def 12 :
theorem
theorem
theorem