:: H\"older's Inequality and {M}inkowski's Inequality
:: by Yasumasa Suzuki
::
:: Received September 25, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

registration
let x be real number ;
cluster right_closed_halfline x ->  non empty ;
coherence
 not right_closed_halfline x is empty
proofend;
end;

theorem :: HOLDER_1:1
for p, q being Real st 0 < p &amp; 0 < q holds
for a being Real st 0 <= a holds
(a to_power p) * (a to_power q) = a to_power (p + q)
proofend;

theorem :: HOLDER_1:2
for p, q being Real st 0 < p &amp; 0 < q holds
for a being Real st 0 <= a holds
(a to_power p) to_power q = a to_power (p * q)
proofend;

theorem Th3: :: HOLDER_1:3
for p being Real st 0 < p holds
for a, b being Real st 0 <= a &amp; a <= b holds
a to_power p <= b to_power p
proofend;

theorem Th4: :: HOLDER_1:4
for p, q, a, b being Real st 1 < p &amp; (1 / p) + (1 / q) = 1 &amp; 0 < a &amp; 0 < b holds
( a * b <= ((a #R p) / p) + ((b #R q) / q) &amp; ( a * b = ((a #R p) / p) + ((b #R q) / q) implies a #R p = b #R q ) &amp; ( a #R p = b #R q implies a * b = ((a #R p) / p) + ((b #R q) / q) ) )
proofend;

theorem Th5: :: HOLDER_1:5
for p, q, a, b being Real st 1 < p &amp; (1 / p) + (1 / q) = 1 &amp; 0 <= a &amp; 0 <= b holds
( a * b <= ((a to_power p) / p) + ((b to_power q) / q) &amp; ( a * b = ((a to_power p) / p) + ((b to_power q) / q) implies a to_power p = b to_power q ) &amp; ( a to_power p = b to_power q implies a * b = ((a to_power p) / p) + ((b to_power q) / q) ) )
proofend;

Lm1:  for a being Real_Sequence st ( for n being Element of NAT holds 0 <= a . n ) holds
for n being Element of NAT holds a . n <= (Partial_Sums a) . n
proofend;

Lm2:  for a being Real_Sequence st ( for n being Element of NAT holds 0 <= a . n ) holds
for n being Element of NAT holds 0 <= (Partial_Sums a) . n
proofend;

Lm3:  for a being Real_Sequence st ( for n being Element of NAT holds 0 <= a . n ) holds
for n being Element of NAT st (Partial_Sums a) . n = 0 holds
for k being Element of NAT st k <= n holds
a . k = 0
proofend;

Lm4:  for a being Real_Sequence
for n being Element of NAT st ( for k being Element of NAT st k <= n holds
a . k = 0 ) holds
(Partial_Sums a) . n = 0
proofend;

begin

theorem Th6: :: HOLDER_1:6
for p, q being Real st 1 < p &amp; (1 / p) + (1 / q) = 1 holds
for a, b, ap, bq, ab being Real_Sequence st ( for n being Element of NAT holds
( ap . n = (abs (a . n)) to_power p &amp; bq . n = (abs (b . n)) to_power q &amp; ab . n = abs ((a . n) * (b . n)) ) ) holds
for n being Element of NAT holds (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))
proofend;

theorem Th7: :: HOLDER_1:7
for p being Real st 1 < p holds
for a, b, ap, bp, ab being Real_Sequence st ( for n being Element of NAT holds
( ap . n = (abs (a . n)) to_power p &amp; bp . n = (abs (b . n)) to_power p &amp; ab . n = (abs ((a . n) + (b . n))) to_power p ) ) holds
for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))
proofend;

theorem Th8: :: HOLDER_1:8
for a, b being Real_Sequence st ( for n being Element of NAT holds a . n <= b . n ) &amp; b is convergent &amp; a is V41() holds
( a is convergent &amp; lim a <= lim b )
proofend;

theorem Th9: :: HOLDER_1:9
for a, b, c being Real_Sequence st ( for n being Element of NAT holds a . n <= (b . n) + (c . n) ) &amp; b is convergent &amp; c is convergent &amp; a is V41() holds
( a is convergent &amp; lim a <= (lim b) + (lim c) )
proofend;

theorem Th10: :: HOLDER_1:10
for p being Real st 0 < p holds
for a, ap being Real_Sequence st a is convergent &amp; ( for n being Element of NAT holds 0 <= a . n ) &amp; ( for n being Element of NAT holds ap . n = (a . n) to_power p ) holds
( ap is convergent &amp; lim ap = (lim a) to_power p )
proofend;

theorem :: HOLDER_1:11
for p being Real st 0 < p holds
for a, ap being Real_Sequence st a is summable &amp; ( for n being Element of NAT holds 0 <= a . n ) &amp; ( for n being Element of NAT holds ap . n = ((Partial_Sums a) . n) to_power p ) holds
( ap is convergent &amp; lim ap = (Sum a) to_power p &amp; ap is V41() &amp; ( for n being Element of NAT holds ap . n <= (Sum a) to_power p ) )
proofend;

theorem :: HOLDER_1:12
for p, q being Real st 1 < p &amp; (1 / p) + (1 / q) = 1 holds
for a, b, ap, bq, ab being Real_Sequence st ( for n being Element of NAT holds
( ap . n = (abs (a . n)) to_power p &amp; bq . n = (abs (b . n)) to_power q &amp; ab . n = abs ((a . n) * (b . n)) ) ) &amp; ap is summable &amp; bq is summable holds
( ab is summable &amp; Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) )
proofend;

theorem :: HOLDER_1:13
for p being Real st 1 < p holds
for a, b, ap, bp, ab being Real_Sequence st ( for n being Element of NAT holds
( ap . n = (abs (a . n)) to_power p &amp; bp . n = (abs (b . n)) to_power p &amp; ab . n = (abs ((a . n) + (b . n))) to_power p ) ) &amp; ap is summable &amp; bp is summable holds
( ab is summable &amp; (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) )
proofend;