TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Generalized Holder inequality puts products into $L^{r}$

Statement

Let $1 \leq p, q, r \leq \infty$ satisfy

$\frac{1}{r} = \frac{1}{p} + \frac{1}{q},$

with the convention $1 / \infty = 0$ . If $f$ and $g$ lie in the corresponding measurable-function spaces ( $L^{p} (μ)$ or $L^{\infty} (μ)$ according to whether the exponent is finite or infinite), then $f g$ lies in the corresponding space for $r$ and

$∥ f g ∥_{r} \leq ∥ f ∥_{p} ∥ g ∥_{q} .$

Facts & Assumptions

Given: Exponents $p, q, r$ with $1 / r = 1 / p + 1 / q$ and measurable functions $f, g$ in the spaces named in the Statement.

[L1]

Holder's inequality for integrals, including the endpoint cases, is available (Holder's inequality for integrals, including the endpoint cases).

[L2]

Conjugate exponents include the endpoint convention $1 / \infty = 0$ (Conjugate exponents, including the endpoint conventions).

[L3]

For $0 < s < \infty$ , $h \in L^{s} (μ)$ means $\int ∣ h ∣^{s} d μ < \infty$ , and $L^{\infty} (μ)$ means finite essential supremum (The function space $L^{p} (μ)$ for $0 < p < \infty$ , The space $L^{\infty} (μ)$ of essentially bounded measurable functions).

[L4]

If $h \in L^{\infty} (μ)$ , then $∣ h ∣ \leq ∥ h ∥_{\infty}$ almost everywhere (The essential supremum is attained as the least essential bound).

Proof

technique · Raise $|fg|$ to the $r$-th power and apply Holder to $|f|^r$ and $|g|^r$ with conjugate exponents $p/r$ and $q/r$

1.1L2L3L4given

If $r = \infty$ , then $1 / p = 1 / q = 0$ , so $p = q = \infty$ by [L2]. Hence $∣ f g ∣ \leq ∥ f ∥_{\infty} ∥ g ∥_{\infty}$ almost everywhere, and taking essential suprema gives $∥ f g ∥_{\infty} \leq ∥ f ∥_{\infty} ∥ g ∥_{\infty} .$ .

1.2L2L3L4given

If $p = \infty$ and $r < \infty$ , then $q = r$ . The pointwise bound and the definition of $∥ g ∥_{r}$ give $∥ f g ∥_{r}^{r} \leq ∥ f ∥_{\infty}^{r} ∥ g ∥_{r}^{r} .$ Indeed, [L4] gives $∣ f ∣ \leq ∥ f ∥_{\infty}$ almost everywhere, so $∣ f g ∣^{r} \leq ∥ f ∥_{\infty}^{r} ∣ g ∣^{r}$ almost everywhere. Taking $r$ -th roots yields the claim. The case $q = \infty$ is symmetric.

1.3L1L2L3givenalgebra

Assume now that $r < \infty$ and $p, q < \infty$ . Then $1 = \frac{r}{p} + \frac{r}{q},$ so the exponents $p / r$ and $q / r$ are conjugate. Because $∣ f ∣^{r} \in L^{p / r} (μ)$ and $∣ g ∣^{r} \in L^{q / r} (μ)$ , [L1] applied to these two functions gives $\int ∣ f g ∣^{r} d μ \leq {(\int ∣ f ∣^{p} d μ)}^{r / p} {(\int ∣ g ∣^{q} d μ)}^{r / q} = ∥ f ∥_{p}^{r} ∥ g ∥_{q}^{r} .$ .

2.1step 1.1step 1.2step 1.3∎

Step 1.1 covers $r = \infty$ , step 1.2 covers the one-infinite endpoint cases, and step 1.3 covers the fully finite case. [step 1.1, step 1.2, step 1.3] In each case $∥ f g ∥_{r} \leq ∥ f ∥_{p} ∥ g ∥_{q}$ , so $f g$ lies in the stated $r$ -space.

Depends on

Used by

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Richard L. Wheeden and Antoni Zygmund, Measure and Integral, Chapter 8 (standard reference, not scraped)
John K. Hunter, Measure Theory, Section 7.2 (standard reference, not scraped)

Generalized Holder inequality puts products into LrLr