begin
theorem Th1:
theorem Th2:
definition
let X be non
empty set ;
let Y be non
empty addLoopStr ;
func FuncAdd X,
Y -> BinOp of
(Funcs X,the carrier of Y) means :
Def1:
for
f,
g being
Element of
Funcs X,the
carrier of
Y holds
it . f,
g = the
addF of
Y .: f,
g;
existence
ex b1 being BinOp of (Funcs X,the carrier of Y) st
for f, g being Element of Funcs X,the carrier of Y holds b1 . f,g = the addF of Y .: f,g
by Th1;
uniqueness
for b1, b2 being BinOp of (Funcs X,the carrier of Y) st ( for f, g being Element of Funcs X,the carrier of Y holds b1 . f,g = the addF of Y .: f,g ) & ( for f, g being Element of Funcs X,the carrier of Y holds b2 . f,g = the addF of Y .: f,g ) holds
b1 = b2
end;
:: deftheorem Def1 defines FuncAdd LOPBAN_1:def 1 :
definition
let X be non
empty set ;
let Y be
RealLinearSpace;
func FuncExtMult X,
Y -> Function of
[:REAL ,(Funcs X,the carrier of Y):],
(Funcs X,the carrier of Y) means :
Def2:
for
a being
Real for
f being
Element of
Funcs X,the
carrier of
Y for
x being
Element of
X holds
(it . [a,f]) . x = a * (f . x);
existence
ex b1 being Function of [:REAL ,(Funcs X,the carrier of Y):],(Funcs X,the carrier of Y) st
for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b1 . [a,f]) . x = a * (f . x)
by Th2;
uniqueness
for b1, b2 being Function of [:REAL ,(Funcs X,the carrier of Y):],(Funcs X,the carrier of Y) st ( for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b1 . [a,f]) . x = a * (f . x) ) & ( for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b2 . [a,f]) . x = a * (f . x) ) holds
b1 = b2
end;
:: deftheorem Def2 defines FuncExtMult LOPBAN_1:def 2 :
:: deftheorem defines FuncZero LOPBAN_1:def 3 :
Lm1:
for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f
theorem Th3:
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
for
X being non
empty set for
Y being
RealLinearSpace 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 Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
for
X being non
empty set for
Y being
RealLinearSpace for
f being
Element of
Funcs X,the
carrier of
Y for
a,
b being
Real holds
(FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),
((FuncExtMult X,Y) . [b,f]) = (FuncExtMult X,Y) . [(a + b),f]
Lm2:
for X being non empty set
for Y being RealLinearSpace
for f, g being Element of Funcs X,the carrier of Y
for a being Real holds (FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),((FuncExtMult X,Y) . [a,g]) = (FuncExtMult X,Y) . [a,((FuncAdd X,Y) . f,g)]
theorem Th13:
definition
let X be non
empty set ;
let Y be
RealLinearSpace;
func RealVectSpace X,
Y -> RealLinearSpace equals
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #);
coherence
RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace
by Th13;
end;
:: deftheorem defines RealVectSpace LOPBAN_1:def 4 :
theorem
theorem
theorem
begin
:: deftheorem LOPBAN_1:def 5 :
canceled;
:: deftheorem Def6 defines homogeneous LOPBAN_1:def 6 :
definition
let X,
Y be
RealLinearSpace;
func LinearOperators X,
Y -> Subset of
(RealVectSpace the carrier of X,Y) means :
Def7:
for
x being
set holds
(
x in it iff
x is
LinearOperator of
X,
Y );
existence
ex b1 being Subset of (RealVectSpace 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 (RealVectSpace 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 Def7 defines LinearOperators LOPBAN_1:def 7 :
theorem Th17:
theorem
for
X,
Y being
RealLinearSpace holds
RLSStruct(#
(LinearOperators X,Y),
(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),
(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),
(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is
Subspace of
RealVectSpace the
carrier of
X,
Y by Th17, RSSPACE:13;
registration
let X,
Y be
RealLinearSpace;
cluster RLSStruct(#
(LinearOperators X,Y),
(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),
(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),
(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is Abelian & RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is add-associative & RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is right_zeroed & RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is right_complementable & RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is vector-distributive & RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is scalar-distributive & RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is scalar-associative & RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is scalar-unital )
by Th17, RSSPACE:13;
end;
definition
let X,
Y be
RealLinearSpace;
func R_VectorSpace_of_LinearOperators X,
Y -> RealLinearSpace equals
RLSStruct(#
(LinearOperators X,Y),
(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),
(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),
(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #);
coherence
RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is RealLinearSpace
;
end;
:: deftheorem defines R_VectorSpace_of_LinearOperators LOPBAN_1:def 8 :
for
X,
Y being
RealLinearSpace holds
R_VectorSpace_of_LinearOperators X,
Y = RLSStruct(#
(LinearOperators X,Y),
(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),
(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),
(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #);
theorem
canceled;
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
begin
theorem Th24:
:: deftheorem Def9 defines bounded LOPBAN_1:def 9 :
theorem Th25:
definition
let X,
Y be
RealNormSpace;
func BoundedLinearOperators X,
Y -> Subset of
(R_VectorSpace_of_LinearOperators X,Y) means :
Def10:
for
x being
set holds
(
x in it iff
x is
bounded LinearOperator of
X,
Y );
existence
ex b1 being Subset of (R_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 (R_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 Def10 defines BoundedLinearOperators LOPBAN_1:def 10 :
theorem Th26:
theorem
for
X,
Y being
RealNormSpace holds
RLSStruct(#
(BoundedLinearOperators X,Y),
(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is
Subspace of
R_VectorSpace_of_LinearOperators X,
Y by Th26, RSSPACE:13;
registration
let X,
Y be
RealNormSpace;
cluster RLSStruct(#
(BoundedLinearOperators X,Y),
(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is Abelian & RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is add-associative & RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is right_zeroed & RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is right_complementable & RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is vector-distributive & RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is scalar-distributive & RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is scalar-associative & RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is scalar-unital )
by Th26, RSSPACE:13;
end;
definition
let X,
Y be
RealNormSpace;
func R_VectorSpace_of_BoundedLinearOperators X,
Y -> RealLinearSpace equals
RLSStruct(#
(BoundedLinearOperators X,Y),
(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #);
coherence
RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is RealLinearSpace
;
end;
:: deftheorem defines R_VectorSpace_of_BoundedLinearOperators LOPBAN_1:def 11 :
for
X,
Y being
RealNormSpace holds
R_VectorSpace_of_BoundedLinearOperators X,
Y = RLSStruct(#
(BoundedLinearOperators X,Y),
(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #);
theorem
canceled;
theorem Th29:
theorem Th30:
theorem Th31:
:: deftheorem Def12 defines modetrans LOPBAN_1:def 12 :
:: deftheorem defines PreNorms LOPBAN_1:def 13 :
theorem Th32:
theorem
theorem Th34:
definition
let X,
Y be
RealNormSpace;
func BoundedLinearOperatorsNorm X,
Y -> Function of
(BoundedLinearOperators X,Y),
REAL means :
Def14:
for
x being
set st
x in BoundedLinearOperators X,
Y holds
it . x = sup (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 = sup (PreNorms (modetrans x,X,Y))
by Th34;
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 = sup (PreNorms (modetrans x,X,Y)) ) & ( for x being set st x in BoundedLinearOperators X,Y holds
b2 . x = sup (PreNorms (modetrans x,X,Y)) ) holds
b1 = b2
end;
:: deftheorem Def14 defines BoundedLinearOperatorsNorm LOPBAN_1:def 14 :
theorem Th35:
theorem Th36:
definition
let X,
Y be
RealNormSpace;
func R_NormSpace_of_BoundedLinearOperators X,
Y -> non
empty NORMSTR equals
NORMSTR(#
(BoundedLinearOperators X,Y),
(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(BoundedLinearOperatorsNorm X,Y) #);
coherence
NORMSTR(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(BoundedLinearOperatorsNorm X,Y) #) is non empty NORMSTR
;
end;
:: deftheorem defines R_NormSpace_of_BoundedLinearOperators LOPBAN_1:def 15 :
for
X,
Y being
RealNormSpace holds
R_NormSpace_of_BoundedLinearOperators X,
Y = NORMSTR(#
(BoundedLinearOperators X,Y),
(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),
(BoundedLinearOperatorsNorm X,Y) #);
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
registration
let X,
Y be
RealNormSpace;
cluster R_NormSpace_of_BoundedLinearOperators X,
Y -> non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealNormSpace-like ;
coherence
( R_NormSpace_of_BoundedLinearOperators X,Y is RealNormSpace-like & R_NormSpace_of_BoundedLinearOperators X,Y is vector-distributive & R_NormSpace_of_BoundedLinearOperators X,Y is scalar-distributive & R_NormSpace_of_BoundedLinearOperators X,Y is scalar-associative & R_NormSpace_of_BoundedLinearOperators X,Y is scalar-unital & R_NormSpace_of_BoundedLinearOperators X,Y is Abelian & R_NormSpace_of_BoundedLinearOperators X,Y is add-associative & R_NormSpace_of_BoundedLinearOperators X,Y is right_zeroed & R_NormSpace_of_BoundedLinearOperators X,Y is right_complementable )
by Th45;
end;
theorem Th46:
begin
:: deftheorem Def16 defines complete LOPBAN_1:def 16 :
Lm3:
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 Th47:
theorem Th48:
theorem Th49: