begin
Lm1:
for rseq being Real_Sequence
for K being real number st ( for n being Element of NAT holds rseq . n <= K ) holds
sup (rng rseq) <= K
Lm2:
for rseq being Real_Sequence st rseq is bounded holds
for n being Element of NAT holds rseq . n <= sup (rng rseq)
:: deftheorem Def1 defines the_set_of_BoundedRealSequences RSSPACE4:def 1 :
Lm3:
RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is Subspace of Linear_Space_of_RealSequences
by RSSPACE:13;
registration
cluster RLSStruct(#
the_set_of_BoundedRealSequences ,
(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),
(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),
(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #)
-> right_complementable Abelian add-associative right_zeroed RealLinearSpace-like ;
coherence
( RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is Abelian & RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is add-associative & RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is right_zeroed & RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is right_complementable & RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is RealLinearSpace-like )
by RSSPACE:13;
end;
Lm4:
( RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is Abelian & RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is add-associative & RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is right_zeroed & RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is right_complementable & RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is RealLinearSpace-like )
;
Lm5:
ex NORM being Function of the_set_of_BoundedRealSequences , REAL st
for x being set st x in the_set_of_BoundedRealSequences holds
NORM . x = sup (rng (abs (seq_id x)))
:: deftheorem Def2 defines linfty_norm RSSPACE4:def 2 :
Lm6:
for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds
( rseq is bounded & sup (rng (abs rseq)) = 0 )
Lm7:
for rseq being Real_Sequence st rseq is bounded & sup (rng (abs rseq)) = 0 holds
for n being Nat holds rseq . n = 0
theorem
canceled;
theorem
registration
cluster NORMSTR(#
the_set_of_BoundedRealSequences ,
(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),
(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),
(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),
linfty_norm #)
-> right_complementable Abelian add-associative right_zeroed RealLinearSpace-like ;
coherence
( NORMSTR(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),linfty_norm #) is Abelian & NORMSTR(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),linfty_norm #) is add-associative & NORMSTR(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),linfty_norm #) is right_zeroed & NORMSTR(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),linfty_norm #) is right_complementable & NORMSTR(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),linfty_norm #) is RealLinearSpace-like )
by Lm4, RSSPACE3:4;
end;
definition
func linfty_Space -> non
empty NORMSTR equals
NORMSTR(#
the_set_of_BoundedRealSequences ,
(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),
(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),
(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),
linfty_norm #);
coherence
NORMSTR(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),linfty_norm #) is non empty NORMSTR
;
end;
:: deftheorem defines linfty_Space RSSPACE4:def 3 :
theorem Th3:
theorem Th4:
theorem
begin
:: deftheorem Def4 defines bounded RSSPACE4:def 4 :
theorem Th6:
:: deftheorem Def5 defines BoundedFunctions RSSPACE4:def 5 :
theorem Th7:
theorem
for
X being non
empty set for
Y being
RealNormSpace holds
RLSStruct(#
(BoundedFunctions X,Y),
(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #) is
Subspace of
RealVectSpace X,
Y by Th7, RSSPACE:13;
registration
let X be non
empty set ;
let Y be
RealNormSpace;
cluster RLSStruct(#
(BoundedFunctions X,Y),
(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #)
-> right_complementable Abelian add-associative right_zeroed RealLinearSpace-like ;
coherence
( RLSStruct(# (BoundedFunctions X,Y),(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #) is Abelian & RLSStruct(# (BoundedFunctions X,Y),(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #) is add-associative & RLSStruct(# (BoundedFunctions X,Y),(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #) is right_zeroed & RLSStruct(# (BoundedFunctions X,Y),(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #) is right_complementable & RLSStruct(# (BoundedFunctions X,Y),(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #) is RealLinearSpace-like )
by Th7, RSSPACE:13;
end;
definition
let X be non
empty set ;
let Y be
RealNormSpace;
func R_VectorSpace_of_BoundedFunctions X,
Y -> RealLinearSpace equals
RLSStruct(#
(BoundedFunctions X,Y),
(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #);
coherence
RLSStruct(# (BoundedFunctions X,Y),(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #) is RealLinearSpace
;
end;
:: deftheorem defines R_VectorSpace_of_BoundedFunctions RSSPACE4:def 6 :
for
X being non
empty set for
Y being
RealNormSpace holds
R_VectorSpace_of_BoundedFunctions X,
Y = RLSStruct(#
(BoundedFunctions X,Y),
(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #);
theorem
canceled;
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem Def7 defines modetrans RSSPACE4:def 7 :
:: deftheorem defines PreNorms RSSPACE4:def 8 :
theorem Th13:
theorem
theorem Th15:
definition
let X be non
empty set ;
let Y be
RealNormSpace;
func BoundedFunctionsNorm X,
Y -> Function of
BoundedFunctions X,
Y,
REAL means :
Def9:
for
x being
set st
x in BoundedFunctions X,
Y holds
it . x = sup (PreNorms (modetrans x,X,Y));
existence
ex b1 being Function of BoundedFunctions X,Y, REAL st
for x being set st x in BoundedFunctions X,Y holds
b1 . x = sup (PreNorms (modetrans x,X,Y))
by Th15;
uniqueness
for b1, b2 being Function of BoundedFunctions X,Y, REAL st ( for x being set st x in BoundedFunctions X,Y holds
b1 . x = sup (PreNorms (modetrans x,X,Y)) ) & ( for x being set st x in BoundedFunctions X,Y holds
b2 . x = sup (PreNorms (modetrans x,X,Y)) ) holds
b1 = b2
end;
:: deftheorem Def9 defines BoundedFunctionsNorm RSSPACE4:def 9 :
theorem Th16:
theorem Th17:
definition
let X be non
empty set ;
let Y be
RealNormSpace;
func R_NormSpace_of_BoundedFunctions X,
Y -> non
empty NORMSTR equals
NORMSTR(#
(BoundedFunctions X,Y),
(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(BoundedFunctionsNorm X,Y) #);
coherence
NORMSTR(# (BoundedFunctions X,Y),(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(BoundedFunctionsNorm X,Y) #) is non empty NORMSTR
;
end;
:: deftheorem defines R_NormSpace_of_BoundedFunctions RSSPACE4:def 10 :
for
X being non
empty set for
Y being
RealNormSpace holds
R_NormSpace_of_BoundedFunctions X,
Y = NORMSTR(#
(BoundedFunctions X,Y),
(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),
(BoundedFunctionsNorm X,Y) #);
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
Lm8:
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 Th28:
theorem Th29: