TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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.

Young's convolution inequality

Statement

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

\frac{1}{r} = \frac{1}{p} + \frac{1}{q} - 1.

If $f \in L^{p} (R^{n})$ and $g \in L^{q} (R^{n})$ , then the convolution $f * g$ is defined almost everywhere and satisfies

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

Facts & Assumptions

Given: Exponents $p, q, r$ as displayed and functions $f \in L^{p}$ , $g \in L^{q}$ .

[L1]

The $L^{1}$ convolution bound is available (If $f, g \in L^{1} (R^{n})$ , then $f * g$ exists almost everywhere, belongs to $L^{1}$ , and $∥ f * g ∥_{1} \leq ∥ f ∥_{1} ∥ g ∥_{1}$ ).

[L2]

Holder's inequality and generalized Holder are available (Holder's inequality for integrals, including the endpoint cases, Generalized Holder inequality puts products into $L^{r}$ , Conjugate exponents, including the endpoint conventions).

[L3]

Minkowski's integral inequality is available (Minkowski's integral inequality).

Proof

technique · direct

1.1

If $r = \infty$ , then $1 / p + 1 / q = 1$ , so $q$ is conjugate to $p$ . For every $x$ , [L2, given, algebra] [L2] gives $∣ f * g (x) ∣ \leq \int ∣ f (x - y) ∣ ∣ g (y) ∣ d y \leq ∥ f ∥_{p} ∥ g ∥_{q} .$ Hence $∥ f * g ∥_{\infty} \leq ∥ f ∥_{p} ∥ g ∥_{q}$ .

L2givenalgebra

1.2

Assume $r < \infty$ . If $r = p$ , interpret the factor [L2, given, algebra] $∣ f (x - y) ∣^{1 - p / r}$ as $1$ and the exponent $p r / (r - p)$ as $\infty$ ; likewise, if $r = q$ , interpret $∣ g (y) ∣^{1 - q / r}$ as $1$ and $q r / (r - q)$ as $\infty$ . With this endpoint convention, generalized Holder from [L2] applies to the three factors $(∣ f (x - y) ∣^{p} ∣ g (y) ∣^{q})^{1 / r}, ∣ f (x - y) ∣^{1 - p / r}, ∣ g (y) ∣^{1 - q / r}$ with exponents $r, \frac{p r}{r - p}, \frac{q r}{r - q},$ because their reciprocals sum to $1 / r + (1 / p - 1 / r) + (1 / q - 1 / r) = 1$ . This yields $∣ f * g (x) ∣^{r} \leq ∥ f ∥_{p}^{r - p} ∥ g ∥_{q}^{r - q} \int ∣ f (x - y) ∣^{p} ∣ g (y) ∣^{q} d y .$

L2givenalgebra

2.1

Integrate the inequality from step 1.2 in $x$ . Tonelli on the nonnegative [L1, L3, step 1.1, step 1.2, algebra] right-hand side gives $∥ f * g ∥_{r}^{r} \leq ∥ f ∥_{p}^{r - p} ∥ g ∥_{q}^{r - q} \iint ∣ f (x - y) ∣^{p} ∣ g (y) ∣^{q} d y d x = ∥ f ∥_{p}^{r} ∥ g ∥_{q}^{r} .$ Taking $r$ th roots proves the finite- $r$ case. Together with step 1.1, this is Young's inequality.

L1L3step 1.1step 1.2algebra∎

Depends on

Used by

Dependency tree · two levels

19 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: An Introduction to Real Analysis (standard reference, not scraped)