begin
theorem Th1:
definition
let X be non
empty set ;
let Y be
ComplexLinearSpace;
func FuncExtMult X,
Y -> Function of
[:COMPLEX ,(Funcs X,the carrier of Y):],
(Funcs X,the carrier of Y) means :
Def1:
for
c being
Complex for
f being
Element of
Funcs X,the
carrier of
Y for
x being
Element of
X holds
(it . [c,f]) . x = c * (f . x);
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)
by Th1;
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;
:: deftheorem Def1 defines FuncExtMult CLOPBAN1:def 1 :
for X being non empty set
for Y being ComplexLinearSpace
for b3 being Function of [:COMPLEX ,(Funcs X,the carrier of Y):],(Funcs X,the carrier of Y) holds
( b3 = FuncExtMult X,Y iff for c being Complex
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b3 . [c,f]) . x = c * (f . x) );
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
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 Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
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 Th11:
definition
let X be non
empty set ;
let Y be
ComplexLinearSpace;
func ComplexVectSpace X,
Y -> ComplexLinearSpace equals
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #);
coherence
CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is ComplexLinearSpace
by Th11;
end;
:: deftheorem defines ComplexVectSpace CLOPBAN1:def 2 :
for X being non empty set
for Y being ComplexLinearSpace holds ComplexVectSpace X,Y = CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #);
theorem
theorem Th13:
begin
:: deftheorem CLOPBAN1:def 3 :
canceled;
:: deftheorem Def4 defines homogeneous CLOPBAN1:def 4 :
for X, Y being non empty CLSStruct
for IT being Function of X,Y holds
( IT is homogeneous iff for x being VECTOR of X
for r being Complex holds IT . (r * x) = r * (IT . x) );
definition
let X,
Y be
ComplexLinearSpace;
func LinearOperators X,
Y -> Subset of
(ComplexVectSpace the carrier of X,Y) means :
Def5:
for
x being
set holds
(
x in it iff
x is
LinearOperator of
X,
Y );
existence
ex b1 being Subset of (ComplexVectSpace the carrier of X,Y) st
for x being set holds
( x in b1 iff x is LinearOperator of X,Y )
uniqueness
for b1, b2 being Subset of (ComplexVectSpace the carrier of X,Y) st ( for x being set holds
( x in b1 iff x is LinearOperator of X,Y ) ) & ( for x being set holds
( x in b2 iff x is LinearOperator of X,Y ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines LinearOperators CLOPBAN1:def 5 :
for X, Y being ComplexLinearSpace
for b3 being Subset of (ComplexVectSpace the carrier of X,Y) holds
( b3 = LinearOperators X,Y iff for x being set holds
( x in b3 iff x is LinearOperator of X,Y ) );
theorem
canceled;
theorem Th15:
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 Th15, CSSPACE:13;
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 Th15, CSSPACE:13;
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 6 :
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
canceled;
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
begin
theorem Th22:
:: deftheorem Def7 defines bounded CLOPBAN1:def 7 :
for X, Y being ComplexNormSpace
for IT being LinearOperator of X,Y holds
( IT is bounded iff ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds ||.(IT . x).|| <= K * ||.x.|| ) ) );
theorem Th23:
definition
let X,
Y be
ComplexNormSpace;
func BoundedLinearOperators X,
Y -> Subset of
(C_VectorSpace_of_LinearOperators X,Y) means :
Def8:
for
x being
set holds
(
x in it iff
x is
bounded LinearOperator of
X,
Y );
existence
ex b1 being Subset of (C_VectorSpace_of_LinearOperators X,Y) st
for x being set holds
( x in b1 iff x is bounded LinearOperator of X,Y )
uniqueness
for b1, b2 being Subset of (C_VectorSpace_of_LinearOperators X,Y) st ( for x being set holds
( x in b1 iff x is bounded LinearOperator of X,Y ) ) & ( for x being set holds
( x in b2 iff x is bounded LinearOperator of X,Y ) ) holds
b1 = b2
end;
:: deftheorem Def8 defines BoundedLinearOperators CLOPBAN1:def 8 :
for X, Y being ComplexNormSpace
for b3 being Subset of (C_VectorSpace_of_LinearOperators X,Y) holds
( b3 = BoundedLinearOperators X,Y iff for x being set holds
( x in b3 iff x is bounded LinearOperator of X,Y ) );
theorem Th24:
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 Th24, CSSPACE:13;
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 Th24, CSSPACE:13;
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 9 :
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)) #);
theorem
canceled;
theorem Th27:
theorem Th28:
theorem Th29:
:: deftheorem Def10 defines modetrans CLOPBAN1:def 10 :
for X, Y being ComplexNormSpace
for f being set st f in BoundedLinearOperators X,Y holds
modetrans f,X,Y = f;
:: deftheorem defines PreNorms CLOPBAN1:def 11 :
for X, Y being ComplexNormSpace
for u being LinearOperator of X,Y holds PreNorms u = { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;
theorem Th30:
theorem
theorem Th32:
definition
let X,
Y be
ComplexNormSpace;
func BoundedLinearOperatorsNorm X,
Y -> Function of
(BoundedLinearOperators X,Y),
REAL means :
Def12:
for
x being
set st
x in BoundedLinearOperators X,
Y holds
it . x = upper_bound (PreNorms (modetrans x,X,Y));
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))
by Th32;
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;
:: deftheorem Def12 defines BoundedLinearOperatorsNorm CLOPBAN1:def 12 :
for X, Y being ComplexNormSpace
for b3 being Function of (BoundedLinearOperators X,Y),REAL holds
( b3 = BoundedLinearOperatorsNorm X,Y iff for x being set st x in BoundedLinearOperators X,Y holds
b3 . x = upper_bound (PreNorms (modetrans x,X,Y)) );
theorem Th33:
theorem Th34:
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 13 :
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) #);
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
registration
let X,
Y be
ComplexNormSpace;
cluster C_NormSpace_of_BoundedLinearOperators X,
Y -> non
empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
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 Th43;
end;
theorem Th44:
begin
:: deftheorem Def14 defines complete CLOPBAN1:def 14 :
for X being ComplexNormSpace holds
( X is complete iff for seq being sequence of X st seq is CCauchy holds
seq is convergent );
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
theorem Th45:
theorem Th46:
theorem Th47: