begin
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))]
begin
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)))) #);
begin
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 set 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 set st x in BoundedLinearOperators (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set 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;
begin
Lm2:
for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e