LemmaStatement: 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.

For $1 < p < \infty$ , the $L^{p}$ norm of a nonnegative function is the supremum of its pairings with $L^{q}$ unit vectors

Statement

Let $1 < p < \infty$ and let $q$ be the conjugate exponent. If $F \in L^{p} (μ)$ is nonnegative, then

$∥ F ∥_{p} = \sup {\int F g d μ : g \geq 0, ∥ g ∥_{q} \leq 1} .$

Facts & Assumptions

Given: $1 < p < \infty$ and a nonnegative function $F \in L^{p} (μ)$ .

[L1]

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

[L2]

Holder's inequality holds for the pairing (Holder's inequality for integrals, including the endpoint cases).

[L3]

The $L^{p}$ norm is the norm on the quotient space (The space $L^{p} (μ)$ as the quotient by null functions, The $L^{p}$ norm descends to the quotient and makes $L^{p}$ a normed space for $1 \leq p \leq \infty$ ).

Proof

technique · direct

1.1

For every $g \geq 0$ with $∥ g ∥_{q} \leq 1$ , [L2] gives [L2, L3, given, algebra] $\int F g d μ \leq ∥ F ∥_{p} ∥ g ∥_{q} \leq ∥ F ∥_{p} .$ So the displayed supremum is at most $∥ F ∥_{p}$ .

L2L3givenalgebra

2.1

If $∥ F ∥_{p} = 0$ , then $F = 0$ almost everywhere and the supremum is also $0$ . [L1, L3, step 1.1, algebra, construct] Otherwise define $g : = \frac{F^{p - 1}}{∥ F ∥_{p}^{p / q}} .$ Because $(p - 1) q = p$ , one has $∥ g ∥_{q}^{q} = \frac{\int F^{(p - 1) q} d μ}{∥ F ∥_{p}^{p}} = 1,$ so $∥ g ∥_{q} = 1$ , and $\int F g d μ = \frac{\int F^{p} d μ}{∥ F ∥_{p}^{p / q}} = ∥ F ∥_{p} .$

L1L3step 1.1algebraconstruct

3.1

Step 1.1 gives the upper bound and step 2.1 attains it, so the supremum [step 1.1, step 2.1] equals $∥ F ∥_{p}$ .

step 1.1step 2.1∎

Depends on

Used by

Minkowski's integral inequality Theorem

Dependency tree · two levels

18 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

John K. Hunter, Measure Theory (standard reference, not scraped)

For 1<p<∞1<p<∞, the LpLp norm of a nonnegative function is the supremum of its pairings with LqLq unit vectors