environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions STRUCT_0, GROUP_1, VECTSP_1, LOPBAN_1, RLVECT_1, ALGSTR_0, FUNCSDOM, NORMSP_0;
theorems ABSVALUE, RLVECT_1, VECTSP_1, BINOP_1, XCMPLX_0, SERIES_1, FUNCT_2, NORMSP_1, SEQ_4, RSSPACE, RSSPACE3, LOPBAN_1, PREPOWER, STRUCT_0, GROUP_1, XREAL_1, XXREAL_0, ALGSTR_0, XREAL_0, NORMSP_0;
schemes BINOP_1, NAT_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;
constructors HIDDEN, REAL_1, INT_2, BINOP_2, PREPOWER, SERIES_1, FUNCSDOM, RSSPACE3, LOPBAN_1, VECTSP_1, SEQ_4, RELSET_1, GROUP_1, SEQ_1;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities STRUCT_0, LOPBAN_1, RLVECT_1, ALGSTR_0, NORMSP_0, RSSPACE;
expansions STRUCT_0, GROUP_1, VECTSP_1, LOPBAN_1, RLVECT_1, FUNCSDOM, NORMSP_0, SEQ_1;
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)) #);