:: LP_SPACE semantic presentation

definition

let x be Real_Sequence;
let p be Real;
func x rto_power p -> Real_Sequence means :Def1: :: LP_SPACE:def 1
for n being Nat holds it . n = (abs (x . n)) to_power p;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines rto_power LP_SPACE:def 1 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines the_set_of_RealSequences_l^ LP_SPACE:def 2 :

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

proof end;

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)

proof end;

theorem Th1: :: LP_SPACE:1

for a, b, c being Real st a >= 0 & a < b & c > 0 holds
a to_power c < b to_power c

proof end;

Lm3: for p being Real st 1 = p holds
for a, b being Real_Sequence
for n being 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))

proof end;

theorem Th2: :: LP_SPACE:2

for p being Real st 1 <= p holds
for a, b being Real_Sequence
for n being 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))

proof end;

Lm4: for a, b being Real_Sequence
for p being Real st 1 = p & a rto_power p is summable & b rto_power p is summable holds
( (a + b) rto_power p is summable & (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)) )

proof end;

theorem Th3: :: LP_SPACE:3

for a, b being Real_Sequence
for p being Real st 1 <= p & a rto_power p is summable & b rto_power p is summable holds
( (a + b) rto_power p is summable & (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)) )

proof end;

theorem Th4: :: LP_SPACE:4

for p being Real st 1 <= p holds
the_set_of_RealSequences_l^ p is lineary-closed

proof end;

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

proof end;

theorem Th6: :: LP_SPACE:6

theorem Th7: :: LP_SPACE:7

Lm5: for p being Real ex NORM 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
NORM . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p)

proof end;

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 by Lm5;
uniqueness

proof end;

end;

:: deftheorem Def3 defines l_norm^ LP_SPACE:def 3 :

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

proof end;

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

proof end;

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 & ( for x being set holds
( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real
for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds
( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) )

proof end;

theorem Th11: :: LP_SPACE:11

for p being Real st p >= 1 holds
for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds
( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 )

proof end;

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 & (Sum (rseq rto_power p)) to_power (1 / p) = 0 holds
for n being Nat holds rseq . n = 0

proof end;

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 (seq_id (a * x)) rto_power p = ((abs a) to_power p) (#) ((seq_id x) rto_power p)

proof end;

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) = ((abs a) to_power p) * (Sum ((seq_id x) rto_power p))

proof end;

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

proof end;

theorem Th13: :: LP_SPACE:13

proof end;

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 RealNormSpace-like

proof end;

theorem Th15: :: LP_SPACE:15

Lm9: 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) )
by RSSPACE3:1;

Lm10: 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 Nat holds rseq . i = (abs ((seq . i) - c)) to_power p ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) to_power p )

proof end;

Lm11: for p being Real st 0 < p holds
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)) to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = ((abs ((lim seq) - c)) to_power p) + (lim seq1) )

proof end;

Lm12: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e holds
lim seq <= e
by RSSPACE2:6;

Lm13: for a, b being Real_Sequence holds a = (a + b) - b

proof end;

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

proof end;

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 CCauchy holds
vseq is convergent

proof end;

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

proof end;

end;

:: deftheorem defines l_Space^ LP_SPACE:def 4 :