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.
A monotone function is differentiable almost everywhere by the rising-sun route
Statement
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()).
Let be monotone. Then is differentiable at Lebesgue-almost every point of .
Facts & Assumptions
Given: Countable choice and a monotone function .
The symbols are those of the statement.
Proof
Replacing by if necessary, we may assume that is nondecreasing. By A nondecreasing function splits uniquely into a jump part and a continuous part, write with continuous and nondecreasing. The continuous theorem A continuous monotone function is differentiable almost everywhere by the rising-sun route gives differentiability of almost everywhere, while A jump function has derivative zero almost everywhere gives almost everywhere.
On the common full-measure set where both derivatives exist, . Therefore exists almost everywhere.
Steps 1.1 and 2.1 prove the theorem.
Depends on
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- A continuous monotone function is differentiable almost everywhere by the rising-sun route
- A countable union of measure-zero sets has measure zero, by countable choice
- The four Dini derivatives always exist in the extended reals, satisfy the one-sided order inequalities, and detect finite differentiability
- A nondecreasing function splits uniquely into a jump part and a continuous part
- A jump function has derivative zero almost everywhere
Used by
- Royden's classical Vitali-covering proof is a third route and is not run on this page Remark
- Every function of bounded variation is differentiable almost everywhere Theorem
- For a nondecreasing function, the derivative is measurable and integrable and its integral is bounded by the total increase Theorem
- Fubini's theorem on term-by-term differentiation for pointwise sums of nondecreasing functions Theorem
Dependency tree · two levels
42 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, Section 1.6 (standard reference, not scraped)
- Frigyes Riesz, Sur l’existence de la dérivée des fonctions monotones et sur quelques problèmes qui s’y rattachent (standard reference, not scraped)