Alphabeta MathHow 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 essential supremum is attained as the least essential bound
Statement
Let be measurable on a measure space , and suppose . Then
Moreover, if and almost everywhere, then
So is the least essential bound of .
Facts & Assumptions
Given: A measurable real-valued function with finite essential supremum .
The essential supremum is the infimum of the essential bounds (The essential supremum of a measurable function with respect to a measure).
Absolute values and threshold sets of measurable functions are measurable (Closure properties of measurable functions used by the integral).
Countable subadditivity bounds the measure of a countable union (Finite and countable subadditivity of measures).
Proof
For each , the number is strictly larger than the infimum in [L1], so it is an essential bound. Therefore the measurable set has measure .
If and almost everywhere, then is one of the essential bounds in [L1], so the infimum satisfies . [L1].
Put . Then is measurable and If , then for every , hence . Therefore almost everywhere.
Step 2.1 proves that itself is an essential bound, and step 1.2 proves that no smaller essential bound exists. Thus is the least essential bound. [step 2.1, step 1.2].
Depends on
Used by
- Convergence in Lᵖ implies convergence in measure Corollary
- Positive, negative, and truncated Sobolev functions Corollary
- Sobolev maxima and minima form a lattice Corollary
- A clipped affine function keeps its zero region Example
- Heat and Poisson semigroups as Fourier multipliers Example
- Multiplicity-two diagonal representation Example
- Pvm of a multiplication operator Example
- Bounded compact data give an everywhere finite Newtonian potential Lemma
- De Giorgi oscillation reduction: one half-level set is small Lemma
- Diagonal multipliers form a von Neumann algebra Lemma
- Exact L2 Fourier multiplier norm Lemma
- Operators commuting with a generating family of multiplications Lemma
- The Radon-Nikodym density of a bounded Lᵖ functional belongs to L^q Lemma
- Null functions form a linear subspace and are exactly the zero-seminorm class Proposition
- On a semifinite measure space, a representing L^q function is unique Proposition
- The functional Λ_g has norm ‖g‖_q; for q=∞ assume μ is semifinite Proposition
- Bounded borel pvm integral Theorem
- Chain rule for a C¹ function with bounded derivative Theorem
- Chain rule for globally Lipschitz scalar maps of Sobolev functions Theorem
- De Giorgi local boundedness of homogeneous subsolutions Theorem
- Finite-measure Lʳ includes into Lᵖ for p < r Theorem
- Generalized Holder inequality puts products into Lʳ Theorem
- Holder's inequality for integrals, including the endpoint cases Theorem
- Koopman operators are linear isometries Theorem
- Lᵖ and L^∞ are vector spaces for p ≥ 1 Theorem
- Lᵖ norms converge to the essential supremum for essentially bounded Lʳ functions Theorem
- Measurable essentially bounded operator fields act decomposably Theorem
- Minkowski's inequality for integrals, including p = ∞ Theorem
- Riesz-Fischer completeness of Lᵖ for 1 ≤ p ≤ ∞ Theorem
- Simple functions are dense in L^∞(μ) in the essential-supremum norm Theorem
- Spectral multiplicity model for separably acting abelian von Neumann algebras Theorem
- The Lᵖ norm descends to the quotient and makes Lᵖ a normed space for 1 ≤ p ≤ ∞ Theorem
- Weak maximum principle for coercive divergence-form equations Theorem
Dependency tree · two levels
12 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, Definition 7.3 and discussion (standard reference, not scraped)
- Richard L. Wheeden and Antoni Zygmund, Measure and Integral, Chapter 8 (standard reference, not scraped)