:: The Banach Space $l^p$
:: by Yasumasa Suzuki
::
:: Received September 25, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

definition
let x be Real_Sequence;
let p be Real;
funcx rto_power p ->  Real_Sequence means :Def1: :: LP_SPACE:def 1
 for n being Element of NAT holds it . n = (abs (x . n)) to_power p;
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = (abs (x . n)) to_power p
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (abs (x . n)) to_power p ) & ( for n being Element of NAT holds b2 . n = (abs (x . n)) to_power p ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines rto_power LP_SPACE:def_1_:_
 for x being Real_Sequence
for p being Real
for b3 being Real_Sequence holds
( b3 = x rto_power p iff for n being Element of NAT holds b3 . n = (abs (x . n)) to_power p );

definition
let p be Real;
assume A1: p >= 1 ;
func the_set_of_RealSequences_l^ p ->  non empty Subset of Linear_Space_of_RealSequences means :Def2: :: LP_SPACE:def 2
 for x being set holds
( x in it iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) );
existence
 ex b1 being non empty 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) rto_power p is summable ) )
proofend;
uniqueness
 for b1, b2 being non empty 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) rto_power p is summable ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines the_set_of_RealSequences_l^ LP_SPACE:def_2_:_
 for p being Real st p >= 1 holds
for b2 being non empty Subset of Linear_Space_of_RealSequences holds
( b2 = the_set_of_RealSequences_l^ p iff for x being set holds
( x in b2 iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) );

Lm1:  for x1, y1 being Real st x1 >= 0 & y1 > 0 holds
x1 to_power y1 >= 0
proofend;

Lm2:  for y1, x1, x2 being Real st y1 > 0 & x1 >= 0 & x2 >= 0 holds
(x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)
proofend;

theorem Th1: :: LP_SPACE:1
for a, b, c being Real st a >= 0 &amp; a < b &amp; c > 0 holds
a to_power c < b to_power c
proofend;

Lm3:  for p being Real st 1 = p holds
for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
proofend;

theorem Th2: :: LP_SPACE:2
for p being Real st 1 <= p holds
for a, b being Real_Sequence
for n being Element of NAT holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))
proofend;

Lm4:  for a, b being Real_Sequence
for p being Real st 1 = p &amp; a rto_power p is summable &amp; b rto_power p is summable holds
( (a + b) rto_power p is summable &amp; (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
proofend;

theorem Th3: :: LP_SPACE:3
for a, b being Real_Sequence
for p being Real st 1 <= p &amp; a rto_power p is summable &amp; b rto_power p is summable holds
( (a + b) rto_power p is summable &amp; (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )
proofend;

theorem Th4: :: LP_SPACE:4
for p being Real st 1 <= p holds
the_set_of_RealSequences_l^ p is linearly-closed
proofend;

theorem Th5: :: LP_SPACE:5
for p being Real st 1 <= p holds
RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is Subspace of Linear_Space_of_RealSequences
proofend;

theorem :: LP_SPACE:6
for p being Real st 1 <= p holds
( RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is Abelian &amp; RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is add-associative &amp; RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is right_zeroed &amp; RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is right_complementable &amp; RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is vector-distributive &amp; RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is scalar-distributive &amp; RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is scalar-associative &amp; RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is scalar-unital ) by Th5;

theorem :: LP_SPACE:7
for p being Real st 1 <= p holds
RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is RealLinearSpace by Th5;

definition
let p be Real;
func l_norm^ p ->  Function of (the_set_of_RealSequences_l^ p),REAL means :Def3: :: LP_SPACE:def 3
 for x being set st x in the_set_of_RealSequences_l^ p holds
it . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p);
existence
 ex b1 being Function of (the_set_of_RealSequences_l^ p),REAL st
for x being set st x in the_set_of_RealSequences_l^ p holds
b1 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p)
proofend;
uniqueness
 for b1, b2 being Function of (the_set_of_RealSequences_l^ p),REAL st ( for x being set st x in the_set_of_RealSequences_l^ p holds
b1 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) &amp; ( for x being set st x in the_set_of_RealSequences_l^ p holds
b2 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines l_norm^ LP_SPACE:def_3_:_
 for p being Real
for b2 being Function of (the_set_of_RealSequences_l^ p),REAL holds
( b2 = l_norm^ p iff for x being set st x in the_set_of_RealSequences_l^ p holds
b2 . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) );

theorem Th8: :: LP_SPACE:8
for p being Real st 1 <= p holds
NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) is RealLinearSpace
proofend;

theorem Th9: :: LP_SPACE:9
for p being Real st p >= 1 holds
NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) is Subspace of Linear_Space_of_RealSequences
proofend;

begin

theorem Th10: :: LP_SPACE:10
for p being Real st 1 <= p holds
for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds
( the carrier of lp = the_set_of_RealSequences_l^ p &amp; ( for x being set holds
( x is VECTOR of lp iff ( x is Real_Sequence &amp; (seq_id x) rto_power p is summable ) ) ) &amp; 0. lp = Zeroseq &amp; ( for x being VECTOR of lp holds x = seq_id x ) &amp; ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) &amp; ( for r being Real
for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) &amp; ( for x being VECTOR of lp holds
( - x = - (seq_id x) &amp; seq_id (- x) = - (seq_id x) ) ) &amp; ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) &amp; ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) &amp; ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) )
proofend;

theorem Th11: :: LP_SPACE:11
for p being Real st p >= 1 holds
for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds
( rseq rto_power p is summable &amp; (Sum (rseq rto_power p)) to_power (1 / p) = 0 )
proofend;

theorem Th12: :: LP_SPACE:12
for p being Real st 1 <= p holds
for rseq being Real_Sequence st rseq rto_power p is summable &amp; (Sum (rseq rto_power p)) to_power (1 / p) = 0 holds
for n being natural number holds rseq . n = 0
proofend;

Lm5:  for p being Real st 1 <= p holds
for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds
for x being Point of lp
for a being Real holds (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p)
proofend;

Lm6:  for p being Real st 1 <= p holds
for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds
for x being Point of lp
for a being Real holds Sum ((seq_id (a * x)) rto_power p) = ((abs a) to_power p) * (Sum ((seq_id x) rto_power p))
proofend;

Lm7:  for p being Real st 1 <= p holds
for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds
for x being Point of lp
for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = (abs a) * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
proofend;

theorem Th13: :: LP_SPACE:13
for p being Real st 1 <= p holds
for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds
for x, y being Point of lp
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. lp ) &amp; ( x = 0. lp implies ||.x.|| = 0 ) &amp; 0 <= ||.x.|| &amp; ||.(x + y).|| <= ||.x.|| + ||.y.|| &amp; ||.(a * x).|| = (abs a) * ||.x.|| )
proofend;

theorem Th14: :: LP_SPACE:14
for p being Real st p >= 1 holds
for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds
( lp is reflexive &amp; lp is discerning &amp; lp is RealNormSpace-like )
proofend;

theorem :: LP_SPACE:15
for p being Real st p >= 1 holds
for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds
lp is RealNormSpace by Th9, Th14;

Lm8:  for p being Real st 0 < p holds
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)) to_power p ) holds
( rseq is convergent &amp; lim rseq = (abs ((lim seq) - c)) to_power p )
proofend;

Lm9:  for p being Real st 0 < p holds
for c being Real
for seq, seq1 being Real_Sequence st seq is convergent &amp; seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((abs ((seq . i) - c)) to_power p) + (seq1 . i) ) holds
( rseq is convergent &amp; lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) )
proofend;

Lm10:  for a, b being Real_Sequence holds a = (a + b) - b
proofend;

Lm11:  for p being Real st p >= 1 holds
for a, b being Real_Sequence st a rto_power p is summable &amp; b rto_power p is summable holds
(a + b) rto_power p is summable
proofend;

theorem Th16: :: LP_SPACE:16
for p being Real st 1 <= p holds
for lp being RealNormSpace st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds
for vseq being sequence of lp st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent
proofend;

definition
let p be Real;
assume A1: 1 <= p ;
func l_Space^ p ->  RealBanachSpace equals :: LP_SPACE:def 4
 NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #);
coherence
 NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) is RealBanachSpace
proofend;
end;

:: deftheorem  defines l_Space^ LP_SPACE:def_4_:_
 for p being Real st 1 <= p holds
l_Space^ p = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #);