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.
The functional has norm ; for assume is semifinite
Statement
Let be a measure space, let , and let be conjugate to . For , let Then If , then equality holds: If and hence , the same equality holds provided is semifinite.
Facts & Assumptions
Given: A measure space , an exponent , its conjugate exponent , and an element .
The pairing functional is bounded and satisfies (Every defines a bounded linear functional on ).
If and is conjugate to , then (Conjugate exponents, including the endpoint conventions).
The essential supremum is the least essential bound: if and is any measurable representative of , then almost everywhere. If and , then the set has positive measure; otherwise would be a smaller essential bound (The essential supremum is attained as the least essential bound).
In a semifinite measure space, every measurable set of positive measure contains a measurable subset of positive finite measure (Finite, sigma-finite, and semifinite measures).
Proof
The upper bound is exactly [L1].
If in , then by definition, so . Hence only the case remains.
Assume . Choose a representative of and define Then by [L2], so Also , so Therefore . Together with step 1.1, this gives .
Assume , so , and assume is semifinite. Put . Step 2.1 leaves only , so . Choose a representative of , and define For , [L3] gives a measurable set of positive measure. By [L4], choose with , and set Then and Hence for every , so . Step 1.1 gives the reverse inequality, and therefore .
Step 2.2 proves the strict-exponent case, and step 3.1 proves the endpoint under semifiniteness. Together with steps 1.1 and 2.1, this proves the proposition.
Depends on
- Every $g\in L^q(\mu)$ defines a bounded linear functional on $L^p(\mu)$
- Conjugate exponents, including the endpoint conventions
- Finite, sigma-finite, and semifinite measures
- The essential supremum is attained as the least essential bound
- Elements of $L^p$ are equivalence classes, so pointwise statements require a representative
Used by
- The Lᵖ norm is the supremum of pairings against unit L^q functions Corollary
- A power function on (0,1] realizes the duality norm on the unit interval Example
- The functional f↦∫₀^1/2 f on Lᵖ[0,1] has norm 2^-1/q Example
- The Radon-Nikodym density of a bounded Lᵖ functional belongs to L^q Lemma
- On a semifinite measure space, a representing L^q function is unique Proposition
- For 1 < p < ∞, the same representation theorem holds on arbitrary measure spaces Theorem
- On a sigma-finite measure space, every bounded linear functional on Lᵖ is integration against a unique L^q function Theorem
Dependency tree · two levels
16 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
- Gerald B. Folland, Real Analysis, 2nd ed., Section 6.2 (standard reference, not scraped)
- Richard F. Bass, Real Analysis for Graduate Students, Proposition 15.10 (standard reference, not scraped)
- John K. Hunter, Measure Theory, Proposition 7.13 (standard reference, not scraped)