:: RSSPACE3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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
ex b1 being Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) )
proof end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_RealSequences st ( for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) ) holds
b1 = b2
proof end;
end;

:: 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: :: RSSPACE3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
not the_set_of_l1RealSequences is empty
proof end;
end;

registration
cluster the_set_of_l1RealSequences -> non empty lineary-closed ;
coherence
the_set_of_l1RealSequences is lineary-closed
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
( 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 RealLinearSpace-like )
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
ex b1 being Function of the_set_of_l1RealSequences , REAL st
for x being set st x in the_set_of_l1RealSequences holds
b1 . x = Sum (abs (seq_id x))
by Lm3;
uniqueness
for b1, b2 being Function of the_set_of_l1RealSequences , REAL st ( for x being set st x in the_set_of_l1RealSequences holds
b1 . x = Sum (abs (seq_id x)) ) & ( for x being set st x in the_set_of_l1RealSequences holds
b2 . x = Sum (abs (seq_id x)) ) holds
b1 = b2
proof end;
end;

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

theorem :: RSSPACE3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RSSPACE3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: RSSPACE3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
func l1_Space -> non empty NORMSTR equals :: RSSPACE3:def 3
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 #);

theorem Th8: :: RSSPACE3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
cluster l1_Space -> non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RealNormSpace-like ;
coherence
( l1_Space is RealNormSpace-like & l1_Space is RealLinearSpace-like & l1_Space is Abelian & l1_Space is add-associative & l1_Space is right_zeroed & l1_Space is right_complementable )
by Lm2, Th4, Th9, NORMSP_1:def 2;
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
||.(x - y).|| is Real
;
end;

:: 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).||;

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 :
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 Nat st
for n1, m1 being Nat st n1 >= k1 & m1 >= k1 holds
dist (seqt . n1),(seqt . m1) < r1 );

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for vseq being sequence of l1_Space st vseq is CCauchy holds
vseq is convergent
proof end;