LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-26 (gpt-6-sol)

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.1L2L3givenalgebra

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

2.1L3step 1.1construct

If $∥ F ∥_{p} = 0$ , then $F = 0$ almost everywhere. Step 1.1 bounds the supremum above by $0$ , while the admissible choice $g = 0$ gives value $0$ , so the supremum is $0$ .

2.2L1L3step 1.1algebraconstruct

If $∥ F ∥_{p} > 0$ , 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} .$

3.1step 1.1step 2.1step 2.2∎

Step 1.1 gives the upper bound and steps 2.1–2.2 attain it in the two cases, so the supremum equals $∥ F ∥_{p}$ .

Depends on

Used by

Minkowski's integral inequality Theorem

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

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