:: H\"older's Inequality and {M}inkowski's Inequality
:: by Yasumasa Suzuki
::
:: Received September 25, 2004
:: Copyright (c) 2004-2011 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

proof end;

end;

theorem :: HOLDER_1:1

for p, q being Real st 0 < p & 0 < q holds
for a being Real st 0 <= a holds
(a to_power p) * (a to_power q) = a to_power (p + q)

proof end;

theorem :: HOLDER_1:2

for p, q being Real st 0 < p & 0 < q holds
for a being Real st 0 <= a holds
(a to_power p) to_power q = a to_power (p * q)

proof end;

theorem Th3: :: HOLDER_1:3

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

proof end;

theorem Th4: :: HOLDER_1:4

for p, q, a, b being Real st 1 < p & (1 / p) + (1 / q) = 1 & 0 < a & 0 < b holds
( a * b <= ((a #R p) / p) + ((b #R q) / q) & ( a * b = ((a #R p) / p) + ((b #R q) / q) implies a #R p = b #R q ) & ( a #R p = b #R q implies a * b = ((a #R p) / p) + ((b #R q) / q) ) )

proof end;

theorem Th5: :: HOLDER_1:5

for p, q, a, b being Real st 1 < p & (1 / p) + (1 / q) = 1 & 0 <= a & 0 <= b holds
( a * b <= ((a to_power p) / p) + ((b to_power q) / q) & ( a * b = ((a to_power p) / p) + ((b to_power q) / q) implies a to_power p = b to_power q ) & ( a to_power p = b to_power q implies a * b = ((a to_power p) / p) + ((b to_power q) / q) ) )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

begin

theorem Th6: :: HOLDER_1:6

for p, q being Real st 1 < p & (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 & bq . n = (abs (b . n)) to_power q & 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))

proof end;

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 & bp . n = (abs (b . n)) to_power p & 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))

proof end;

theorem Th8: :: HOLDER_1:8

for a, b being Real_Sequence st ( for n being Element of NAT holds a . n <= b . n ) & b is convergent & a is non-decreasing holds
( a is convergent & lim a <= lim b )

proof end;

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) ) & b is convergent & c is convergent & a is non-decreasing holds
( a is convergent & lim a <= (lim b) + (lim c) )

proof end;

theorem Th10: :: HOLDER_1:10

for p being Real st 0 < p holds
for a, ap being Real_Sequence st a is convergent & ( for n being Element of NAT holds 0 <= a . n ) & ( for n being Element of NAT holds ap . n = (a . n) to_power p ) holds
( ap is convergent & lim ap = (lim a) to_power p )

proof end;

theorem :: HOLDER_1:11

for p being Real st 0 < p holds
for a, ap being Real_Sequence st a is summable & ( for n being Element of NAT holds 0 <= a . n ) & ( for n being Element of NAT holds ap . n = ((Partial_Sums a) . n) to_power p ) holds
( ap is convergent & lim ap = (Sum a) to_power p & ap is non-decreasing & ( for n being Element of NAT holds ap . n <= (Sum a) to_power p ) )

proof end;

theorem :: HOLDER_1:12

for p, q being Real st 1 < p & (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 & bq . n = (abs (b . n)) to_power q & ab . n = abs ((a . n) * (b . n)) ) ) & ap is summable & bq is summable holds
( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) )

proof end;

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 & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) & ap is summable & bp is summable holds
( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) )

proof end;