:: by Yasumasa Suzuki, Noboru Endou and Yasunari Shidama

::

:: Received August 8, 2003

:: Copyright (c) 2003-2012 Association of Mizar Users

begin

definition

ex b_{1} being Subset of Linear_Space_of_RealSequences st

for x being set holds

( x in b_{1} iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) )

for b_{1}, b_{2} being Subset of Linear_Space_of_RealSequences st ( for x being set holds

( x in b_{1} iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) ) holds

b_{1} = b_{2}
end;

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 for x being set holds

( x in it iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines the_set_of_l1RealSequences RSSPACE3:def 1 :

for b_{1} being Subset of Linear_Space_of_RealSequences holds

( b_{1} = the_set_of_l1RealSequences iff for x being set holds

( x in b_{1} iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) );

for b

( b

( x in b

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 Element of NAT holds rseq . i = abs ((seq . i) - c) ) holds

( rseq is convergent & lim rseq = abs ((lim seq) - c) )

for seq being Real_Sequence st seq is convergent holds

for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = abs ((seq . i) - c) ) holds

( rseq is convergent & lim rseq = abs ((lim seq) - c) )

proof 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:11;

registration

( 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:11;

end;

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:11;

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

;

definition

ex b_{1} being Function of the_set_of_l1RealSequences,REAL st

for x being set st x in the_set_of_l1RealSequences holds

b_{1} . x = Sum (abs (seq_id x))

for b_{1}, b_{2} being Function of the_set_of_l1RealSequences,REAL st ( for x being set st x in the_set_of_l1RealSequences holds

b_{1} . x = Sum (abs (seq_id x)) ) & ( for x being set st x in the_set_of_l1RealSequences holds

b_{2} . x = Sum (abs (seq_id x)) ) holds

b_{1} = b_{2}
end;

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 for x being set st x in the_set_of_l1RealSequences holds

it . x = Sum (abs (seq_id x));

ex b

for x being set st x in the_set_of_l1RealSequences holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines l_norm RSSPACE3:def 2 :

for b_{1} being Function of the_set_of_l1RealSequences,REAL holds

( b_{1} = l_norm iff for x being set st x in the_set_of_l1RealSequences holds

b_{1} . x = Sum (abs (seq_id x)) );

for b

( b

b

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;

coherence

not NORMSTR(# X,Z,A,M,N #) is empty ;

end;
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;

coherence

not NORMSTR(# X,Z,A,M,N #) is empty ;

theorem :: RSSPACE3:2

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

l is RealLinearSpace by RSSPACE:15;

l is RealLinearSpace by RSSPACE:15;

theorem Th3: :: RSSPACE3:3

for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds

( rseq is absolutely_summable & Sum (abs rseq) = 0 )

( rseq is absolutely_summable & Sum (abs rseq) = 0 )

proof end;

theorem Th4: :: RSSPACE3:4

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

for n being Element of NAT holds rseq . n = 0

for n being Element of NAT holds rseq . n = 0

proof end;

definition

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;

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 #);

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 ;

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

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 Th6: :: RSSPACE3:6

( 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)) ) )

( 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 Th7: :: RSSPACE3:7

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

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

( l1_Space is reflexive & l1_Space is discerning & l1_Space is RealNormSpace-like & l1_Space is vector-distributive & l1_Space is scalar-distributive & l1_Space is scalar-associative & l1_Space is scalar-unital & l1_Space is Abelian & l1_Space is add-associative & l1_Space is right_zeroed & l1_Space is right_complementable )
end;

cluster l1_Space -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;

coherence ( l1_Space is reflexive & l1_Space is discerning & l1_Space is RealNormSpace-like & l1_Space is vector-distributive & l1_Space is scalar-distributive & l1_Space is scalar-associative & l1_Space is scalar-unital & l1_Space is Abelian & l1_Space is add-associative & l1_Space is right_zeroed & l1_Space is right_complementable )

proof end;

Lm3: 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) )

proof end;

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

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

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

notation

let NRM be non empty NORMSTR ;

let seqt be sequence of NRM;

synonym Cauchy_sequence_by_Norm seqt for CCauchy ;

end;
let seqt be sequence of NRM;

synonym Cauchy_sequence_by_Norm seqt for CCauchy ;

theorem Th8: :: RSSPACE3:8

for NRM being RealNormSpace

for seq being sequence of NRM holds

( seq is Cauchy_sequence_by_Norm iff for r being Real st r > 0 holds

ex k being Element of NAT st

for n, m being Element of NAT st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < r )

for seq being sequence of NRM holds

( seq is Cauchy_sequence_by_Norm iff for r being Real st r > 0 holds

ex k being Element of NAT st

for n, m being Element of NAT st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < r )

proof end;