begin
theorem Th1:
theorem Th2:
for
X,
Y,
Z being
RealNormSpace 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
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
Element of
BoundedLinearOperators X,
X;
func f + g -> Element of
BoundedLinearOperators X,
X equals
(Add_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X)) . f,
g;
correctness
coherence
(Add_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X)) . f,g is Element of BoundedLinearOperators X,X;
;
end;
:: deftheorem defines + LOPBAN_2:def 1 :
definition
let X be
RealNormSpace;
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 LOPBAN_1:def 10;
end;
:: deftheorem defines * LOPBAN_2:def 2 :
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
(Mult_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X)) . a,
f;
correctness
coherence
(Mult_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X)) . a,f is Element of BoundedLinearOperators X,X;
;
end;
:: deftheorem defines * LOPBAN_2:def 3 :
definition
let X be
RealNormSpace;
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 LOPBAN_2:def 4 :
theorem Th3:
:: deftheorem defines FuncUnit LOPBAN_2:def 5 :
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
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)) #);
theorem Th13:
theorem Th14:
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)) #);
theorem Th15:
theorem
theorem Th17:
theorem Th18:
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) #);
theorem Th19:
theorem Th20:
:: deftheorem defines Banach_Algebra-like_1 LOPBAN_2:def 9 :
:: deftheorem Def10 defines Banach_Algebra-like_2 LOPBAN_2:def 10 :
:: deftheorem defines Banach_Algebra-like_3 LOPBAN_2:def 11 :
:: deftheorem Def12 defines Banach_Algebra-like LOPBAN_2:def 12 :
theorem
theorem
theorem