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.
Lebesgue differentiation theorem on
Statement
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()).
Let . Then for Lebesgue-almost every .
Facts & Assumptions
Given: The Axiom of Countable Choice and a function .
Continuous compactly supported functions are recovered by small ball averages at every point. (Continuous compactly supported functions are recovered by small ball averages)
For , is dense in . ( is dense in for )
Chebyshev-Markov controls superlevel sets by the integral. (Chebyshev-Markov inequality for the integral)
The centered maximal operator is weak type . (The centered Hardy-Littlewood maximal operator is weak type )
Under Countable Choice, is a complete measure on the Lebesgue sigma-algebra of (Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume). For measurable sets, finite and countable unions have measure at most the corresponding sum, and inclusion implies monotonicity (Finite and countable subadditivity of measures, Measures are monotone). In particular a countable union of measurable -zero sets has measure zero.
Proof
For each integer and each integer , apply [L2] to the [L2, given, choose, construct] function and choose such that Set
Let [L3, L4, L5, step 1.1, algebra] Both sets are Lebesgue measurable: the maximal superlevel set is open by the ball-average continuity argument in [L4], and is measurable. Finite subadditivity [L5], [L4] and [L3] give
For fixed , put [step 2.1, algebra] The sets , their countable unions, and are measurable by [L5]. By countable subadditivity [L5] and step 2.1 For every , inclusion and monotonicity [L5] give . Given , choose with ; thus . This uses small positive tail measures, without asserting that any is null.
Let . Then there is such that [L1, step 1.1, step 3.1, algebra] for every . Fix such a and take . Since , one has , so Therefore Now [L1] gives , so for every . Letting yields .
The bad set for radius differentiation is contained in [step 3.1, step 4.1, L5] , which is null by [L5]. Thus the convergence holds for almost every .
Depends on
- The average of a locally integrable function over a Euclidean ball
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- A locally integrable function on $\mathbb{R}^n$
- Continuous compactly supported functions are recovered by small ball averages
- $C_c(\mathbb{R}^n)$ is dense in $L^p(\mathbb{R}^n)$ for $1 \le p < \infty$
- Chebyshev-Markov inequality for the integral
- The centered Hardy-Littlewood maximal operator is weak type $(1,1)$
- Assuming countable choice, $\mathcal{L}(\mathbb{R}^n)$ is a sigma-algebra containing every elementary set and $\lambda_n$ is a complete measure extending elementary volume
- Finite and countable subadditivity of measures
- Measures are monotone
Used by
- A locally integrable function can fail to differentiate on a null set Example
- Analytic quasiconformality gives both quadrilateral modulus bounds Lemma
- Circular dilatation, quasisymmetry and the analytic definition Lemma
- Distribution decay from maximal cubes for Aₚ weights Lemma
- Moser iteration for positive supersolutions: negative-power and logarithmic comparison Lemma
- Almost every point is a Lebesgue point of a locally integrable function Theorem
- Existence and uniqueness for projected dynamics and convergence of projection Euler under countable and dependent choice Theorem
- Local L¹ contraction for two entropy solutions Theorem
- Morrey's inequality for p>n Theorem
- Rademacher differentiability in Euclidean space Theorem
- RNP and almost-everywhere differentiability of Lipschitz curves Theorem
- The geometric and analytic definitions of quasiconformality agree Theorem
- The mean-zero Poincare inequality on bounded John domains Theorem
- W^1,∞ functions on convex domains have Lipschitz representatives Theorem
Dependency tree · two levels
48 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
- Terence Tao, An Introduction to Measure Theory, Theorem 1.6.11 and Exercise 1.6.14 (standard reference, not scraped)
- Gerald B. Folland, Real Analysis: Modern Techniques and Their Applications, 2nd ed., Theorem 3.18 (standard reference, not scraped)