Loading [MathJax]/extensions/tex2jax.js
Lm1:
for x1, y1 being Real st x1 >= 0 & y1 > 0 holds
x1 to_power y1 >= 0
Lm2:
for x1, x2, y1 being Real st y1 > 0 & x1 >= 0 & x2 >= 0 holds
(x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)
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))
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)) )
theorem
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 &
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 &
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 &
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 &
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 &
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 &
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 &
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;
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 = (|.a.| to_power p) (#) ((seq_id x) rto_power p)
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) = (|.a.| to_power p) * (Sum ((seq_id x) rto_power p))
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) = |.a.| * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))
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 Nat holds rseq . i = |.((seq . i) - c).| to_power p ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| to_power p )
Lm9:
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 = (|.((seq . i) - c).| to_power p) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| to_power p) + (lim seq1) )
Lm10:
for a, b being Real_Sequence holds a = (a + b) - b
Lm11:
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