:: Banach Space of Absolute Summable Real Sequences
:: by Yasumasa Suzuki, Noboru Endou and Yasunari Shidama
::
:: Copyright (c) 2003-2021 Association of Mizar Users

definition
func the_set_of_l1RealSequences -> Subset of Linear_Space_of_RealSequences means :Def1: :: RSSPACE3:def 1
for x being object 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 object 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 object holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) ) & ( for x being object 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 object holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) );

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 = |.((seq . i) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| )
proof end;

registration
coherence
proof end;
end;

registration end;

Lm1:

Lm2:
;

definition
func l_norm -> Function of the_set_of_l1RealSequences,REAL means :Def2: :: RSSPACE3:def 2
for x being object st x in the_set_of_l1RealSequences holds
it . x = Sum (abs ());
existence
ex b1 being Function of the_set_of_l1RealSequences,REAL st
for x being object st x in the_set_of_l1RealSequences holds
b1 . x = Sum (abs ())
proof end;
uniqueness
for b1, b2 being Function of the_set_of_l1RealSequences,REAL st ( for x being object st x in the_set_of_l1RealSequences holds
b1 . x = Sum (abs ()) ) & ( for x being object st x in the_set_of_l1RealSequences holds
b2 . x = Sum (abs ()) ) 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 object st x in the_set_of_l1RealSequences holds
b1 . x = Sum (abs ()) );

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;

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

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;

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;

( 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 = () + () ) & ( for r being Real
for u being VECTOR of l1_Space holds r * u = r (#) () ) & ( for u being VECTOR of l1_Space holds
( - u = - () & seq_id (- u) = - () ) ) & ( for u, v being VECTOR of l1_Space holds u - v = () - () ) & ( for v being VECTOR of l1_Space holds seq_id v is absolutely_summable ) & ( for v being VECTOR of l1_Space holds = Sum (abs ()) ) )
proof end;

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

registration
coherence by ;
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 Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((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 :: 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 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 ;
end;