begin
:: deftheorem Def1 defines the_set_of_l1RealSequences RSSPACE3:def 1 :
for b1 being Subset of Linear_Space_of_RealSequences holds
( b1 = the_set_of_l1RealSequences iff for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) );
theorem Th1:
Lm1:
RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is Subspace of Linear_Space_of_RealSequences
by RSSPACE:13;
registration
cluster RLSStruct(#
the_set_of_l1RealSequences,
(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),
(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),
(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is Abelian & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is add-associative & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is right_zeroed & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is right_complementable & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is vector-distributive & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is scalar-distributive & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is scalar-associative & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is scalar-unital )
by RSSPACE:13;
end;
Lm2:
RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is RealLinearSpace
;
Lm3:
ex NORM being Function of the_set_of_l1RealSequences,REAL st
for x being set st x in the_set_of_l1RealSequences holds
NORM . x = Sum (abs (seq_id x))
:: deftheorem Def2 defines l_norm RSSPACE3:def 2 :
for b1 being Function of the_set_of_l1RealSequences,REAL holds
( b1 = l_norm iff for x being set st x in the_set_of_l1RealSequences holds
b1 . x = Sum (abs (seq_id x)) );
registration
let X be non
empty set ;
let Z be
Element of
X;
let A be
BinOp of
X;
let M be
Function of
[:REAL,X:],
X;
let N be
Function of
X,
REAL;
cluster NORMSTR(#
X,
Z,
A,
M,
N #)
-> non
empty ;
coherence
not NORMSTR(# X,Z,A,M,N #) is empty
;
end;
theorem
canceled;
theorem
canceled;
theorem
theorem Th5:
theorem Th6:
theorem Th7:
definition
func l1_Space -> non
empty NORMSTR equals
NORMSTR(#
the_set_of_l1RealSequences,
(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),
(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),
(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),
l_norm #);
coherence
NORMSTR(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),l_norm #) is non empty NORMSTR
;
end;
:: deftheorem defines l1_Space RSSPACE3:def 3 :
l1_Space = NORMSTR(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),l_norm #);
begin
theorem Th8:
theorem Th9:
Lm4:
for c being Real
for seq, seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) )
:: deftheorem defines dist RSSPACE3:def 4 :
for X being non empty NORMSTR
for x, y being Point of X holds dist (x,y) = ||.(x - y).||;
:: deftheorem Def5 defines CCauchy RSSPACE3:def 5 :
for NRM being non empty NORMSTR
for seqt being sequence of NRM holds
( seqt is CCauchy iff for r1 being Real st r1 > 0 holds
ex k1 being Element of NAT st
for n1, m1 being Element of NAT st n1 >= k1 & m1 >= k1 holds
dist ((seqt . n1),(seqt . m1)) < r1 );
theorem Th10:
theorem