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 .
Statement references
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 ()
A locally integrable function on
Continuous compactly supported functions are recovered by small ball averages
is dense in for
Chebyshev-Markov inequality for the integral
The centered Hardy-Littlewood maximal operator is weak type
Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume
Finite and countable subadditivity of measures
Measures are monotone