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.
The indefinite integral of an function is differentiable almost everywhere
Statement
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()).
Let and let . Fix a measurable integrable representative, also denoted by , if is interpreted as a space of almost-everywhere equivalence classes. Define Then there is a measurable set whose complement in has Lebesgue measure zero such that is differentiable at every and The primitive is independent of the chosen representative; the almost-everywhere derivative identity holds for every fixed measurable integrable representative.
Statement references
Facts & Assumptions
Given: The Axiom of Countable Choice, reals , and the measurable integrable representative fixed in the Statement.
The norm is the integral of the absolute value. (The class of integrable functions)
Differentiation along families shrinking nicely recovers the point value at almost every point. (Differentiation holds along families shrinking nicely)
Proof
Extend by outside , obtaining a function on [L1, given, construct, algebra] . Because is bounded by on and vanishes elsewhere, so . For and every , define Each family shrinks nicely to with constant , because and .
Apply [L2] to the set and the family from step [L2, step 1.1, algebra] 1.1. This gives a full-measure subset such that Applying [L2] again to the family gives another full-measure subset such that Hence both one-sided limits hold for every , which still has full measure in . At such an , if is small then while for , Both one-sided limits therefore equal .
Take from step 2.1. It is measurable and has full measure in , and for every . If almost everywhere, then their integrals on every interval agree, so they define the same . Removing also the null set on which their values differ gives on a full-measure set. Thus the conclusion holds for every fixed representative.