environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FUNCT_1, ZFMISC_1, XCMPLX_0, FUNCOP_1, SUBSET_1, FUNCT_2, RELAT_1, PARTFUN1, CLVECT_1, STRUCT_0, RLVECT_1, LOPBAN_1, SUPINF_2, ARYTM_3, ARYTM_1, COMPLEX1, ALGSTR_0, MONOID_0, TARSKI, MSSUBFAM, UNIALG_1, RLSUB_1, RSSPACE, NAT_1, PRE_TOPC, SEQ_2, ORDINAL2, NORMSP_1, XXREAL_0, CARD_1, REAL_1, XXREAL_2, SEQ_4, REWRITE1, RSSPACE3, SEQ_1, VALUED_1, CLOPBAN1, METRIC_1, RELAT_2, FCONT_1, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, PRE_TOPC, DOMAIN_1, FUNCOP_1, BINOP_1, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, MONOID_0, NUMBERS, RLVECT_1, NORMSP_0, NORMSP_1, VALUED_1, SEQ_1, SEQ_2, SEQ_4, FUNCSDOM, CLVECT_1, CSSPACE, CSSPACE3, LOPBAN_1, VECTSP_1;
definitions FUNCT_1, ALGSTR_0, VECTSP_1, NORMSP_0, XXREAL_2;
theorems ALGSTR_0, XBOOLE_0, TARSKI, ABSVALUE, RLVECT_1, FUNCOP_1, XREAL_0, XCMPLX_0, SEQ_1, SEQ_2, FUNCT_1, NAT_1, FUNCT_2, SEQ_4, FUNCT_3, CLVECT_1, LOPBAN_1, CSSPACE, COMPLEX1, CSSPACE3, MONOID_0, XREAL_1, XXREAL_0, NORMSP_1, VECTSP_1, NORMSP_0, ORDINAL1;
schemes SEQ_1, FUNCT_2, XBOOLE_0, BINOP_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, MONOID_0, CLVECT_1, CSSPACE3, VALUED_1, VALUED_0, SEQ_4, FUNCT_1, NAT_1, SEQ_1, SEQ_2;
constructors HIDDEN, DOMAIN_1, REAL_1, COMPLEX1, FUNCSDOM, MONOID_0, LOPBAN_1, CSSPACE3, SEQ_4, RELSET_1, BINOP_2, SEQ_2, COMSEQ_2, FUNCT_3, SEQ_1;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities BINOP_1, STRUCT_0, ALGSTR_0, NORMSP_0;
expansions FUNCT_1, BINOP_1, NORMSP_0;
definition
let X be non
empty set ;
let Y be
ComplexLinearSpace;
existence
ex b1 being Function of [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st
for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b1 . [c,f]) . x = c * (f . x)
uniqueness
for b1, b2 being Function of [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st ( for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b1 . [c,f]) . x = c * (f . x) ) & ( for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b2 . [c,f]) . x = c * (f . x) ) holds
b1 = b2
end;
theorem Th4:
for
X being non
empty set for
Y being
ComplexLinearSpace for
f,
g,
h being
Element of
Funcs (
X, the
carrier of
Y) holds
(FuncAdd (X,Y)) . (
f,
((FuncAdd (X,Y)) . (g,h)))
= (FuncAdd (X,Y)) . (
((FuncAdd (X,Y)) . (f,g)),
h)
theorem Th9:
for
X being non
empty set for
Y being
ComplexLinearSpace for
f being
Element of
Funcs (
X, the
carrier of
Y)
for
a,
b being
Complex holds
(FuncAdd (X,Y)) . (
((FuncExtMult (X,Y)) . [a,f]),
((FuncExtMult (X,Y)) . [b,f]))
= (FuncExtMult (X,Y)) . [(a + b),f]
Lm1:
for X being non empty set
for Y being ComplexLinearSpace
for f, g being Element of Funcs (X, the carrier of Y)
for a being Complex holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
theorem
for
X,
Y being
ComplexLinearSpace holds
CLSStruct(#
(LinearOperators (X,Y)),
(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),
(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),
(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is
Subspace of
ComplexVectSpace ( the
carrier of
X,
Y)
by Th13, CSSPACE:11;
registration
let X,
Y be
ComplexLinearSpace;
cluster CLSStruct(#
(LinearOperators (X,Y)),
(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),
(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),
(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is Abelian & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is add-associative & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is right_zeroed & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is right_complementable & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is vector-distributive & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is scalar-distributive & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is scalar-associative & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is scalar-unital )
by Th13, CSSPACE:11;
end;
definition
let X,
Y be
ComplexLinearSpace;
func C_VectorSpace_of_LinearOperators (
X,
Y)
-> ComplexLinearSpace equals
CLSStruct(#
(LinearOperators (X,Y)),
(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),
(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),
(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #);
coherence
CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is ComplexLinearSpace
;
end;
::
deftheorem defines
C_VectorSpace_of_LinearOperators CLOPBAN1:def 5 :
for X, Y being ComplexLinearSpace holds C_VectorSpace_of_LinearOperators (X,Y) = CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #);
theorem
for
X,
Y being
ComplexNormSpace holds
CLSStruct(#
(BoundedLinearOperators (X,Y)),
(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),
(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),
(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is
Subspace of
C_VectorSpace_of_LinearOperators (
X,
Y)
by Th21, CSSPACE:11;
registration
let X,
Y be
ComplexNormSpace;
cluster CLSStruct(#
(BoundedLinearOperators (X,Y)),
(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),
(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),
(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is Abelian & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is add-associative & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is right_zeroed & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is right_complementable & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is vector-distributive & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-distributive & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-associative & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-unital )
by Th21, CSSPACE:11;
end;
definition
let X,
Y be
ComplexNormSpace;
func C_VectorSpace_of_BoundedLinearOperators (
X,
Y)
-> ComplexLinearSpace equals
CLSStruct(#
(BoundedLinearOperators (X,Y)),
(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),
(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),
(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #);
coherence
CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is ComplexLinearSpace
;
end;
::
deftheorem defines
C_VectorSpace_of_BoundedLinearOperators CLOPBAN1:def 8 :
for X, Y being ComplexNormSpace holds C_VectorSpace_of_BoundedLinearOperators (X,Y) = CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #);
definition
let X,
Y be
ComplexNormSpace;
existence
ex b1 being Function of (BoundedLinearOperators (X,Y)),REAL st
for x being object st x in BoundedLinearOperators (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
uniqueness
for b1, b2 being Function of (BoundedLinearOperators (X,Y)),REAL st ( for x being object st x in BoundedLinearOperators (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in BoundedLinearOperators (X,Y) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b1 = b2
end;
definition
let X,
Y be
ComplexNormSpace;
func C_NormSpace_of_BoundedLinearOperators (
X,
Y)
-> non
empty CNORMSTR equals
CNORMSTR(#
(BoundedLinearOperators (X,Y)),
(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),
(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),
(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),
(BoundedLinearOperatorsNorm (X,Y)) #);
coherence
CNORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #) is non empty CNORMSTR
;
end;
::
deftheorem defines
C_NormSpace_of_BoundedLinearOperators CLOPBAN1:def 12 :
for X, Y being ComplexNormSpace holds C_NormSpace_of_BoundedLinearOperators (X,Y) = CNORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);
registration
let X,
Y be
ComplexNormSpace;
coherence
( C_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & C_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace-like & C_NormSpace_of_BoundedLinearOperators (X,Y) is vector-distributive & C_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-distributive & C_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-associative & C_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-unital & C_NormSpace_of_BoundedLinearOperators (X,Y) is Abelian & C_NormSpace_of_BoundedLinearOperators (X,Y) is add-associative & C_NormSpace_of_BoundedLinearOperators (X,Y) is right_zeroed & C_NormSpace_of_BoundedLinearOperators (X,Y) is right_complementable )
by Th38;
end;
Lm2:
for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e holds
lim seq <= e