:: RSSPACE3 semantic presentation

definition

func the_set_of_l1RealSequences -> Subset of Linear_Space_of_RealSequences means :Def1: :: RSSPACE3:def 1
for x being set holds
( x in it iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines the_set_of_l1RealSequences RSSPACE3:def 1 :

theorem Th1: :: RSSPACE3:1

for c being Real
for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = abs ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = abs ((lim seq) - c) )

proof end;

registration

cluster the_set_of_l1RealSequences -> non empty ;
coherence

proof end;

end;

registration

cluster the_set_of_l1RealSequences -> non empty lineary-closed ;
coherence

proof end;

end;

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 ) #) -> Abelian add-associative right_zeroed right_complementable RealLinearSpace-like ;
coherence 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))

proof end;

definition

func l_norm -> Function of the_set_of_l1RealSequences , REAL means :Def2: :: RSSPACE3:def 2
for x being set st x in the_set_of_l1RealSequences holds
it . x = Sum (abs (seq_id x));
existence by Lm3;
uniqueness

proof end;

end;

:: deftheorem Def2 defines l_norm RSSPACE3:def 2 :

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 by STRUCT_0:def 1;

end;

theorem :: RSSPACE3:2

canceled;

theorem :: RSSPACE3:3

canceled;

theorem Th4: :: RSSPACE3:4

for l being NORMSTR st RLSStruct(# the carrier of l,the Zero of l,the add of l,the Mult of l #) is RealLinearSpace holds
l is RealLinearSpace

proof end;

theorem Th5: :: RSSPACE3:5

for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds
( rseq is absolutely_summable & Sum (abs rseq) = 0 )

proof end;

theorem Th6: :: RSSPACE3:6

for rseq being Real_Sequence st rseq is absolutely_summable & Sum (abs rseq) = 0 holds
for n being Nat holds rseq . n = 0

proof end;

theorem Th7: :: RSSPACE3:7

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 RealLinearSpace by Lm2, Th4;

definition end;

:: deftheorem defines l1_Space RSSPACE3:def 3 :

theorem Th8: :: RSSPACE3:8

( the carrier of l1_Space = the_set_of_l1RealSequences & ( for x being set holds
( x is VECTOR of l1_Space iff ( x is Real_Sequence & seq_id x is absolutely_summable ) ) ) & 0. l1_Space = Zeroseq & ( for u being VECTOR of l1_Space holds u = seq_id u ) & ( for u, v being VECTOR of l1_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of l1_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of l1_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of l1_Space holds seq_id v is absolutely_summable ) & ( for v being VECTOR of l1_Space holds ||.v.|| = Sum (abs (seq_id v)) ) )

proof end;

theorem Th9: :: RSSPACE3:9

for x, y being Point of l1_Space
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. l1_Space ) & ( x = 0. l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )

proof end;

registration end;

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 Nat holds rseq . i = (abs ((seq . i) - c)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) )

proof end;

definition

let X be non empty NORMSTR ;
let x, y be Point of X;
func dist x,y -> Real equals :: RSSPACE3:def 4
||.(x - y).||;
coherence ;

end;

:: deftheorem defines dist RSSPACE3:def 4 :

definition

let NRM be non empty NORMSTR ;
let seqt be sequence of NRM;
attr seqt is CCauchy means :Def5: :: RSSPACE3:def 5
for r1 being Real st r1 > 0 holds
ex k1 being Nat st
for n1, m1 being Nat st n1 >= k1 & m1 >= k1 holds
dist (seqt . n1),(seqt . m1) < r1;

end;

:: deftheorem Def5 defines CCauchy RSSPACE3:def 5 :

notation

let NRM be non empty NORMSTR ;
let seqt be sequence of NRM;
synonym Cauchy_sequence_by_Norm seqt for CCauchy seqt;

end;

theorem Th10: :: RSSPACE3:10

for NRM being non empty RealNormSpace
for seq being sequence of NRM holds
( seq is CCauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )

proof end;

theorem :: RSSPACE3:11

for vseq being sequence of l1_Space st vseq is CCauchy holds
vseq is convergent

proof end;