environ
vocabularies HIDDEN, NUMBERS, SEQ_1, REAL_1, SUBSET_1, FUNCT_1, COMPLEX1, POWER, XXREAL_0, XBOOLE_0, RSSPACE, SERIES_1, CARD_1, TARSKI, RELAT_1, ARYTM_3, CARD_3, RLVECT_1, RSSPACE3, NORMSP_1, RLSUB_1, XXREAL_2, VALUED_0, VALUED_1, ALGSTR_0, ZFMISC_1, STRUCT_0, SUPINF_2, REALSET1, ARYTM_1, SEQ_2, ORDINAL2, PRE_TOPC, NAT_1, LOPBAN_1, LP_SPACE, NORMSP_0, METRIC_1, RELAT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, REALSET1, PARTFUN1, FUNCT_2, PRE_TOPC, DOMAIN_1, XXREAL_0, XREAL_0, XCMPLX_0, ORDINAL1, NUMBERS, RLVECT_1, COMPLEX1, REAL_1, NAT_1, STRUCT_0, ALGSTR_0, RLSUB_1, NORMSP_0, NORMSP_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1, POWER, RSSPACE, RSSPACE3, LOPBAN_1;
definitions TARSKI, NORMSP_0;
theorems XBOOLE_0, RELAT_1, TARSKI, ABSVALUE, ZFMISC_1, SEQ_1, SEQM_3, SERIES_1, COMSEQ_3, FUNCT_1, NAT_1, SEQ_2, FUNCT_2, RLVECT_1, RLSUB_1, NORMSP_1, XREAL_0, RSSPACE2, XCMPLX_1, SEQ_4, POWER, RSSPACE, RSSPACE3, LOPBAN_1, HOLDER_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1;
schemes NAT_1, SEQ_1, FUNCT_2, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, REALSET1, STRUCT_0, RLVECT_1, LOPBAN_1, VALUED_0, RSSPACE, VALUED_1, FUNCT_2, SERIES_1;
constructors HIDDEN, REAL_1, COMPLEX1, SEQ_2, PREPOWER, SERIES_1, REALSET1, RLSUB_1, RSSPACE3, LOPBAN_1, RELSET_1, BINOP_2, COMSEQ_2, BINOP_1, FUNCSDOM, SEQ_1;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities REALSET1, BINOP_1, RLVECT_1, STRUCT_0, ALGSTR_0, VALUED_1, NORMSP_0, RSSPACE, SEQ_1, FUNCSDOM;
expansions NORMSP_0;
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