:: H\"older's Inequality and {M}inkowski's Inequality
::  by Yasumasa Suzuki
::
:: Received September 25, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, REAL_1, LIMFUNC1, XBOOLE_0, XXREAL_0, CARD_1, ARYTM_3,
      POWER, RELAT_1, PREPOWER, ARYTM_1, PARTFUN1, FUNCT_1, FDIFF_1, VALUED_1,
      SUBSET_1, TARSKI, XXREAL_1, ORDINAL2, SEQ_1, SERIES_1, VALUED_0,
      COMPLEX1, SEQ_2, XXREAL_2, NAT_1, FUNCT_2, FCONT_1, CARD_3, FUNCT_7;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, FUNCT_1, FUNCT_2,
      LIMFUNC1, RCOMP_1, FCONT_1, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1,
      ORDINAL1, NUMBERS, REAL_1, NAT_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2,
      SEQ_2, SERIES_1, FDIFF_1, PREPOWER, POWER, TAYLOR_1, RECDEF_1;
 constructors PARTFUN1, REAL_1, NAT_1, INT_2, SEQ_2, SEQM_3, RCOMP_1, RFUNCT_2,
      FCONT_1, LIMFUNC1, FDIFF_1, PREPOWER, SERIES_1, TAYLOR_1, VALUED_1,
      RECDEF_1, RELSET_1, COMSEQ_2, NUMBERS;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
      MEMBERED, RCOMP_1, VALUED_0, VALUED_1, FUNCT_2, SEQ_2, SEQ_4, FCONT_3,
      NAT_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: H\"older 's inequality

reserve a, b, p, q for Real;

registration
  let x be Real;
  cluster right_closed_halfline(x) -> non empty;
end;

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

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

theorem :: HOLDER_1:3
  for p be Real st 0 <= p
  for a,b be Real st 0 <= a & a <= b holds
  a to_power p <= b to_power p;

theorem :: HOLDER_1:4
  1 < p & 1/p + 1/q = 1 & 0 < a & 0 < b implies a * b <= a #R p / p
  + b #R q / q & (a * b = a #R p / p + b #R q / q iff a #R p= b #R q);

theorem :: HOLDER_1:5
  1 < p & 1/p + 1/q = 1 & 0 <= a & 0 <= b implies a * b <= a
to_power p / p + b to_power q / q & (a * b = a to_power p / p + b to_power q /
  q iff a to_power p = b to_power q);

begin  :: Minkowski's inequality

theorem :: HOLDER_1:6
  for p, q be Real st 1 < p & 1/p + 1/q = 1
  for a,b,ap,bq,ab be
Real_Sequence st ( for n be Nat holds ap.n=|.a.n.| to_power p & bq.
n=|.b.n.| to_power q & ab.n=|.a.n* b.n.|) holds for n be Nat holds
Partial_Sums(ab).n <= ( (Partial_Sums(ap).n) to_power (1/p) ) * ( (Partial_Sums
  (bq).n) to_power (1/q) );

theorem :: HOLDER_1:7
  for p be Real st 1 < p
  for a,b,ap,bp,ab be Real_Sequence st ( for
n be Nat holds ap.n=|.a.n.| to_power p & bp.n=|.b.n.| to_power p &
  ab.n=|.a.n+b.n.| to_power p ) holds for n be 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);

theorem :: HOLDER_1:8
  for a,b be Real_Sequence st (for n be Nat holds a.n <=
b.n ) & b is convergent & a is non-decreasing holds a is convergent & lim a <=
  lim b;

theorem :: HOLDER_1:9
  for a,b,c be Real_Sequence st (for n be 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;

theorem :: HOLDER_1:10
  for p be Real st 0 < p
for a,ap be Real_Sequence st a is
  convergent & (for n be Nat holds 0 <=a.n ) &
   (for n be Nat holds ap.n=(a.n) to_power p)
holds ap is convergent & lim ap = (lim a) to_power p;

theorem :: HOLDER_1:11
  for p be Real st 0 < p for a,ap be Real_Sequence st a is summable & (
for n be Nat holds 0 <=a.n ) & (for n be 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 be Nat holds ap.n <= Sum(a
  ) to_power p;

theorem :: HOLDER_1:12
  for p, q be Real st 1 < p & 1/p + 1/q = 1 for a,b,ap,bq,ab be
Real_Sequence st ( for n be Nat holds ap.n=|.a.n.| to_power p & bq.
n=|.b.n.| to_power q & ab.n=|.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) );

theorem :: HOLDER_1:13
  for p be Real st 1 < p for a,b,ap,bp,ab be Real_Sequence st ( for n be
Nat holds ap.n=|.a.n.| to_power p & bp.n=|.b.n.| to_power p & ab.n
  =|.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);