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_BoundedComplexSequences CSSPACE4:def 1 :
Lm3:
for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded
Lm4:
for c being Complex
for seq being Complex_Sequence st seq is bounded holds
c (#) seq is bounded
Lm5:
CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is Subspace of Linear_Space_of_ComplexSequences
by CSSPACE:13;
registration
cluster CLSStruct(#
the_set_of_BoundedComplexSequences ,
(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),
(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),
(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is Abelian & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is add-associative & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is right_zeroed & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is right_complementable & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is vector-distributive & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is scalar-distributive & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is scalar-associative & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is scalar-unital )
by CSSPACE:13;
end;
Lm6:
( CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is Abelian & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is add-associative & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is right_zeroed & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is right_complementable & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is vector-distributive & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is scalar-distributive & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is scalar-associative & CLSStruct(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ) #) is scalar-unital )
;
Lm7:
ex NORM being Function of the_set_of_BoundedComplexSequences ,REAL st
for x being set st x in the_set_of_BoundedComplexSequences holds
NORM . x = sup (rng |.(seq_id x).|)
:: deftheorem Def2 defines Complex_linfty_norm CSSPACE4:def 2 :
Lm8:
for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds
( seq is bounded & sup (rng |.seq.|) = 0 )
Lm9:
for seq being Complex_Sequence st seq is bounded holds
|.seq.| is bounded
Lm10:
for seq being Complex_Sequence st |.seq.| is bounded holds
seq is bounded
Lm11:
for seq being Complex_Sequence st seq is bounded & sup (rng |.seq.|) = 0 holds
for n being Element of NAT holds seq . n = 0c
theorem
canceled;
theorem
registration
cluster CNORMSTR(#
the_set_of_BoundedComplexSequences ,
(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),
(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),
(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),
Complex_linfty_norm #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is Abelian & CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is add-associative & CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is right_zeroed & CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is right_complementable & CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is vector-distributive & CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is scalar-distributive & CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is scalar-associative & CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is scalar-unital )
by Lm6, CSSPACE3:4;
end;
definition
func Complex_linfty_Space -> non
empty CNORMSTR equals
CNORMSTR(#
the_set_of_BoundedComplexSequences ,
(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),
(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),
(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),
Complex_linfty_norm #);
coherence
CNORMSTR(# the_set_of_BoundedComplexSequences ,(Zero_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_BoundedComplexSequences ,Linear_Space_of_ComplexSequences ),Complex_linfty_norm #) is non empty CNORMSTR
;
end;
:: deftheorem defines Complex_linfty_Space CSSPACE4:def 3 :
theorem Th3:
theorem Th4:
Lm12:
for seq1, seq2, seq3 being Complex_Sequence holds
( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) )
theorem Th5:
theorem
begin
:: deftheorem Def4 defines bounded CSSPACE4:def 4 :
theorem Th7:
:: deftheorem Def5 defines ComplexBoundedFunctions CSSPACE4:def 5 :
theorem Th8:
theorem
for
X being non
empty set for
Y being
ComplexNormSpace holds
CLSStruct(#
(ComplexBoundedFunctions X,Y),
(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is
Subspace of
ComplexVectSpace X,
Y by Th8, CSSPACE:13;
registration
let X be non
empty set ;
let Y be
ComplexNormSpace;
cluster CLSStruct(#
(ComplexBoundedFunctions X,Y),
(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is Abelian & CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is add-associative & CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is right_zeroed & CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is right_complementable & CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is vector-distributive & CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is scalar-distributive & CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is scalar-associative & CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is scalar-unital )
by Th8, CSSPACE:13;
end;
definition
let X be non
empty set ;
let Y be
ComplexNormSpace;
func C_VectorSpace_of_BoundedFunctions X,
Y -> ComplexLinearSpace equals
CLSStruct(#
(ComplexBoundedFunctions X,Y),
(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #);
coherence
CLSStruct(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #) is ComplexLinearSpace
;
end;
:: deftheorem defines C_VectorSpace_of_BoundedFunctions CSSPACE4:def 6 :
for
X being non
empty set for
Y being
ComplexNormSpace holds
C_VectorSpace_of_BoundedFunctions X,
Y = CLSStruct(#
(ComplexBoundedFunctions X,Y),
(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)) #);
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
:: deftheorem Def7 defines modetrans CSSPACE4:def 7 :
:: deftheorem defines PreNorms CSSPACE4:def 8 :
theorem Th14:
theorem
theorem Th16:
definition
let X be non
empty set ;
let Y be
ComplexNormSpace;
func ComplexBoundedFunctionsNorm X,
Y -> Function of
(ComplexBoundedFunctions X,Y),
REAL means :
Def9:
for
x being
set st
x in ComplexBoundedFunctions X,
Y holds
it . x = sup (PreNorms (modetrans x,X,Y));
existence
ex b1 being Function of (ComplexBoundedFunctions X,Y),REAL st
for x being set st x in ComplexBoundedFunctions X,Y holds
b1 . x = sup (PreNorms (modetrans x,X,Y))
by Th16;
uniqueness
for b1, b2 being Function of (ComplexBoundedFunctions X,Y),REAL st ( for x being set st x in ComplexBoundedFunctions X,Y holds
b1 . x = sup (PreNorms (modetrans x,X,Y)) ) & ( for x being set st x in ComplexBoundedFunctions X,Y holds
b2 . x = sup (PreNorms (modetrans x,X,Y)) ) holds
b1 = b2
end;
:: deftheorem Def9 defines ComplexBoundedFunctionsNorm CSSPACE4:def 9 :
theorem Th17:
theorem Th18:
definition
let X be non
empty set ;
let Y be
ComplexNormSpace;
func C_NormSpace_of_BoundedFunctions X,
Y -> non
empty CNORMSTR equals
CNORMSTR(#
(ComplexBoundedFunctions X,Y),
(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(ComplexBoundedFunctionsNorm X,Y) #);
coherence
CNORMSTR(# (ComplexBoundedFunctions X,Y),(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),(ComplexBoundedFunctionsNorm X,Y) #) is non empty CNORMSTR
;
end;
:: deftheorem defines C_NormSpace_of_BoundedFunctions CSSPACE4:def 10 :
for
X being non
empty set for
Y being
ComplexNormSpace holds
C_NormSpace_of_BoundedFunctions X,
Y = CNORMSTR(#
(ComplexBoundedFunctions X,Y),
(Zero_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Add_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(Mult_ (ComplexBoundedFunctions X,Y),(ComplexVectSpace X,Y)),
(ComplexBoundedFunctionsNorm X,Y) #);
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
registration
let X be non
empty set ;
let Y be
ComplexNormSpace;
cluster C_NormSpace_of_BoundedFunctions X,
Y -> non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
coherence
( C_NormSpace_of_BoundedFunctions X,Y is ComplexNormSpace-like & C_NormSpace_of_BoundedFunctions X,Y is vector-distributive & C_NormSpace_of_BoundedFunctions X,Y is scalar-distributive & C_NormSpace_of_BoundedFunctions X,Y is scalar-associative & C_NormSpace_of_BoundedFunctions X,Y is scalar-unital & C_NormSpace_of_BoundedFunctions X,Y is Abelian & C_NormSpace_of_BoundedFunctions X,Y is add-associative & C_NormSpace_of_BoundedFunctions X,Y is right_zeroed & C_NormSpace_of_BoundedFunctions X,Y is right_complementable )
by Th27;
end;
theorem Th28:
Lm13:
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 Th29:
theorem Th30:
begin
theorem
theorem
theorem
theorem