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.
Finite-measure includes into for
Statement
Let be a measure space with .
- If and , then and
- If and , then and
Facts & Assumptions
Given: A finite measure space .
Holder's inequality for integrals is available (Holder's inequality for integrals, including the endpoint cases).
Conjugate exponents are defined in Conjugate exponents, including the endpoint conventions.
and are the measurable-function spaces of The function space for and The space of essentially bounded measurable functions.
If , then almost everywhere (The essential supremum is attained as the least essential bound).
Proof
Suppose and put Then and , so [L2] makes them conjugate. Apply [L1] to the functions and : Taking -th roots gives the claimed bound.
If , then Indeed, almost everywhere by [L4]. Thus and .
Steps 1.1 and 1.2 prove the finite-measure inclusion laws. [step 1.1, step 1.2].
Depends on
- Holder's inequality for integrals, including the endpoint cases
- Conjugate exponents, including the endpoint conventions
- The function space $\mathcal{L}^p(\mu)$ for $0 < p < \infty$
- The space $L^\infty(\mu)$ of essentially bounded measurable functions
- The essential supremum is attained as the least essential bound
Used by
- Conditional lp contraction Corollary
- Lyapunov's moment inequality on a probability space Corollary
- One-dimensional W^1,p functions have unique absolutely continuous representatives Corollary
- Positive, negative, and truncated Sobolev functions Corollary
- Fourier coefficients and trigonometric polynomials on the torus Definition
- A clipped affine function keeps its zero region Example
- Poincare on an interval: the length dependence is linear Example
- Ball-mean oscillation bound by the Riesz potential of the gradient Lemma
- Band-limited samples are the Fourier coefficients of the rescaled spectrum Lemma
- Ergodic averages converge in Lp on finite-measure spaces Lemma
- Uniform Lp bounds for periodic Fourier partial sums Lemma
- Chain rule for a C¹ function with bounded derivative Theorem
- Chain rule for globally Lipschitz scalar maps of Sobolev functions Theorem
- Hausdorff–Young for periodic Fourier coefficients Theorem
- Khinchin weak law for integrable IID variables Theorem
- L^q convergence implies Lᵖ convergence on a probability space Theorem
- The Fourier basis and Parseval's identity on the finite torus Theorem
- The Marcel Riesz conjugate-function theorem on the circle Theorem
- The trigonometric system is complete in L² of the torus Theorem
- W^1,∞ functions on convex domains have Lipschitz representatives Theorem
Dependency tree · two levels
17 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, Theorem 8.2 (standard reference, not scraped)
- John K. Hunter, Measure Theory, Chapter 17 overview (standard reference, not scraped)