environ
vocabularies HIDDEN, NUMBERS, CLVECT_1, LOPBAN_1, RELAT_1, RLVECT_1, FUNCT_1, ARYTM_3, XXREAL_2, NORMSP_1, XXREAL_0, PRE_TOPC, CLOPBAN1, CARD_1, REAL_1, SUBSET_1, RSSPACE, LOPBAN_2, BINOP_1, STRUCT_0, COMPLEX1, ALGSTR_0, XBOOLE_0, GROUP_1, SUPINF_2, MESFUNC1, FUNCSDOM, VECTSP_1, LATTICES, CFUNCDOM, CSSPACE3, REWRITE1, NAT_1, RSSPACE3, SEQ_2, ZFMISC_1, XCMPLX_0, PREPOWER, COMSEQ_1, SERIES_1, CSSPACE, ARYTM_1, CLOPBAN2, NORMSP_0, METRIC_1, RELAT_2, SEQ_4, FCONT_1;
notations HIDDEN, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, PARTFUN1, FUNCT_2, PRE_TOPC, BINOP_1, STRUCT_0, ALGSTR_0, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1, NUMBERS, XXREAL_2, REAL_1, RLVECT_1, VALUED_1, SEQ_4, COMPLEX1, GROUP_1, VECTSP_1, SERIES_1, COMSEQ_1, COMSEQ_3, NORMSP_0, CLVECT_1, CSSPACE, CSSPACE3, CLOPBAN1, CFUNCDOM, PREPOWER;
definitions STRUCT_0, GROUP_1, VECTSP_1, CLOPBAN1, RLVECT_1, ALGSTR_0, CLVECT_1, CFUNCDOM, NORMSP_0;
theorems ABSVALUE, RLVECT_1, VECTSP_1, XCMPLX_0, SERIES_1, FUNCT_2, SEQ_4, PREPOWER, STRUCT_0, CLOPBAN1, CLVECT_1, COMPLEX1, CSSPACE3, COMSEQ_3, CSSPACE, GROUP_1, XREAL_1, XXREAL_0, ALGSTR_0, VALUED_1, NORMSP_0;
schemes BINOP_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, CLVECT_1, CSSPACE3, CLOPBAN1, CFUNCDOM, ALGSTR_0, VALUED_1, VALUED_0, NORMSP_0;
constructors HIDDEN, REAL_1, PREPOWER, COMSEQ_3, CSSPACE3, CLOPBAN1, CFUNCDOM, VECTSP_1, SEQ_4, RELSET_1, BINOP_2, BINOP_1, GROUP_1;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities STRUCT_0, CLOPBAN1, BINOP_1, ALGSTR_0, CLVECT_1, NORMSP_0;
expansions STRUCT_0, GROUP_1, VECTSP_1, CLOPBAN1, BINOP_1, RLVECT_1, ALGSTR_0, CLVECT_1, CFUNCDOM;
theorem Th2:
for
X,
Y,
Z being
ComplexNormSpace 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
ComplexNormSpace;
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
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)))) #);
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)))) #);
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)) #);