TheoremStatement: Literature-sourcedProof: AI-generatedprecheck 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.

Lyapunov interpolation inequality for $L^{p}$ norms

Statement

Let $1 \leq p_{0} < p < p_{1} < \infty$ and let $θ \in (0, 1)$ satisfy

$\frac{1}{p} = \frac{θ}{p_{0}} + \frac{1 - θ}{p_{1}} .$

If $f \in L^{p_{0}} (μ) \cap L^{p_{1}} (μ)$ , then $f \in L^{p} (μ)$ and

$∥ f ∥_{p} \leq ∥ f ∥_{p_{0}}^{θ} ∥ f ∥_{p_{1}}^{1 - θ} .$

Facts & Assumptions

Given: Exponents $p_{0} < p < p_{1}$ and a function $f \in L^{p_{0}} (μ) \cap L^{p_{1}} (μ)$ .

[L1]

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

[L2]

Conjugate exponents are defined in Conjugate exponents, including the endpoint conventions.

[L3]

Membership in $L^{s} (μ)$ means finiteness of the $s$ -power integral (The function space $L^{p} (μ)$ for $0 < p < \infty$ ).

Proof

Proof technique: If $1 / p = θ / p_{0} + (1 - θ) / p_{1}$ , rewrite $∣ f ∣^{p}$ as the product $∣ f ∣^{θ p} ∣ f ∣^{(1 - θ) p}$ and apply Holder with conjugate exponents $p_{0} / (θ p)$ and $p_{1} / ((1 - θ) p)$ .

1.1

Put [L1, L2, L3, given, algebra] $a : = \frac{p_{0}}{θ p}, b : = \frac{p_{1}}{(1 - θ) p} .$ Then $\frac{1}{a} + \frac{1}{b} = \frac{θ p}{p_{0}} + \frac{(1 - θ) p}{p_{1}} = 1,$ so [L2] makes $a$ and $b$ conjugate exponents. Also ${(∣ f ∣^{θ p})}^{a} = ∣ f ∣^{p_{0}}, {(∣ f ∣^{(1 - θ) p})}^{b} = ∣ f ∣^{p_{1}} .$ Applying [L1] to the factors $∣ f ∣^{θ p}$ and $∣ f ∣^{(1 - θ) p}$ therefore yields $\int ∣ f ∣^{p} d μ \leq {(\int ∣ f ∣^{p_{0}} d μ)}^{θ p / p_{0}} {(\int ∣ f ∣^{p_{1}} d μ)}^{(1 - θ) p / p_{1}} = ∥ f ∥_{p_{0}}^{θ p} ∥ f ∥_{p_{1}}^{(1 - θ) p} .$

2.1

Taking $p$ -th roots yields the Lyapunov interpolation inequality, and the right-hand side is finite by [L3], so $f \in L^{p} (μ)$ .

step 1.1L3∎

Depends on

Used by

Lyapunov inequality is equivalent to log-convexity of the reciprocal-exponent norm profile Remark

Dependency tree · two levels

13 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 6.3 (standard reference, not scraped)

Lyapunov interpolation inequality for LpLp norms