:: H\"older's Inequality and {M}inkowski's Inequality
:: by Yasumasa Suzuki
::
:: Received September 25, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem :: HOLDER_1:1
theorem :: HOLDER_1:2
theorem Th3: :: HOLDER_1:3
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) ) )
theorem Th5: :: HOLDER_1:5
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
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
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
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
theorem Th6: :: HOLDER_1:6
theorem Th7: :: HOLDER_1:7
theorem Th8: :: HOLDER_1:8
theorem Th9: :: HOLDER_1:9
theorem Th10: :: HOLDER_1:10
theorem :: HOLDER_1:11
theorem :: HOLDER_1:12
theorem :: HOLDER_1:13