begin
theorem Th2:
for
X,
Y,
Z being
RealNormSpace for
f being
Lipschitzian LinearOperator of
X,
Y for
g being
Lipschitzian LinearOperator of
Y,
Z holds
(
g * f is
Lipschitzian LinearOperator of
X,
Z & ( for
x being
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;
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;
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
coherence
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)))) #) is doubleLoopStr ;
;
end;
::
deftheorem defines
Ring_of_BoundedLinearOperators LOPBAN_2:def 6 :
for X being RealNormSpace holds Ring_of_BoundedLinearOperators X = 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)))) #);
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
coherence
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)))) #) is AlgebraStr ;
;
end;
::
deftheorem defines
R_Algebra_of_BoundedLinearOperators LOPBAN_2:def 7 :
for X being RealNormSpace holds R_Algebra_of_BoundedLinearOperators X = 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)))) #);
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
coherence
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)) #) is Normed_AlgebraStr ;
;
end;
::
deftheorem defines
R_Normed_Algebra_of_BoundedLinearOperators LOPBAN_2:def 8 :
for X being RealNormSpace holds R_Normed_Algebra_of_BoundedLinearOperators X = 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)) #);