Holder and Minkowski inequalities in integral form

Let $(X,\mathcal{A},\mu )$ be a measure space and for measurable $f$ put $\mathrm{\parallel }f{\mathrm{\parallel }}_p:=({\int }_X\mathrm{\mid }f{\mathrm{\mid }}^{p}d\mu {)}^{1\mathrm{/}p}$ for $1\le p<\mathrm{\infty }$, and $\mathrm{\parallel }f{\mathrm{\parallel }}_{\mathrm{\infty }}:={\mathrm{ess\hspace{0.17em}sup}}_X\mathrm{\mid }f\mathrm{\mid }$.

Holder. If $1\le p,q\le \mathrm{\infty }$ with $\frac{1}{p}+\frac{1}{q}=1$, then for all measurable $f,g$,

${\int }_X\mathrm{\mid }fg\mathrm{\mid }d\mu \le \mathrm{\parallel }f{\mathrm{\parallel }}_p\mathrm{\parallel }g{\mathrm{\parallel }}_q\mathrm{.}$

For $1<p<\mathrm{\infty }$ equality holds exactly when $\mathrm{\mid }f{\mathrm{\mid }}^p$ and $\mathrm{\mid }g{\mathrm{\mid }}^q$ are proportional almost everywhere. The case $p=q=2$ is the Cauchy-Schwarz inequality for the integral.

Minkowski. If $1\le p\le \mathrm{\infty }$, then for all measurable $f,g$,

$\mathrm{\parallel }f+g{\mathrm{\parallel }}_p\le \mathrm{\parallel }f{\mathrm{\parallel }}_p+\mathrm{\parallel }g{\mathrm{\parallel }}_p\mathrm{.}$

Hence $\mathrm{\parallel }\cdot {\mathrm{\parallel }}_p$ is a seminorm on the measurable functions with finite $p$-th moment, and a norm on the quotient by equality almost everywhere. For $0<p<1$ Minkowski's inequality reverses on nonnegative functions and $\mathrm{\parallel }\cdot {\mathrm{\parallel }}_p$ is not a norm.

Not proved in this library. The inequalities are recorded here in their integral form only, and used in no proof here.

What would prove it. Young's inequality $ab\le a^p\mathrm{/}p+b^q\mathrm{/}q$, or the concavity of the logarithm, plus the monotonicity and additivity of the Lebesgue integral (Lebesgue measure and the Lebesgue integral ‡). No convergence theorem is needed; the proofs are the finite-sum proofs with sums replaced by integrals.

Which page it serves. The roots and rational powers page already proves the weighted arithmetic-geometric mean inequality and the finite forms of Holder and Minkowski for finite sequences of reals with rational exponents, and the ${\mathbb{R}}^n$ as a normed space page uses those to get the $p$-norms on ${\mathbb{R}}^n$. The integral form is the same statement for the counting measure replaced by an arbitrary measure, and it is exactly the step that needs the integral.

What is genuinely missing here, and what is not. The inequality itself is not deep and its finite version is in scope. What is deferred is the setting: the statement quantifies over measurable functions and uses $\int$ and $\mathrm{ess\hspace{0.17em}sup}$, none of which this library defines. The moment the integral exists, these two lines follow at once, which is why they are recorded together rather than as separate results.