Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck pass
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 L1 function is differentiable almost everywhere

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)).

Let a<b and let f∈L1([a,b]). Fix a measurable integrable representative, also denoted by f, if L1([a,b]) is interpreted as a space of almost-everywhere equivalence classes. Define F(x):=∫axf(t) dt(a≤x≤b). Then there is a measurable set E⊆(a,b) whose complement in (a,b) has Lebesgue measure zero such that F is differentiable at every x∈E and F′(x)=f(x)(x∈E). The primitive F is independent of the chosen representative; the almost-everywhere derivative identity holds for every fixed measurable integrable representative.

Facts & Assumptions

Given: The Axiom of Countable Choice, reals a<b, and the measurable integrable representative f fixed in the Statement.

[L1]

The L1 norm is the integral of the absolute value. (The class L1(μ) of integrable functions)

[L2]

Differentiation along families shrinking nicely recovers the point value at almost every point. (Differentiation holds along families shrinking nicely)

Proof

technique · direct
1.1L1givenconstructalgebra

Extend f by 0 outside [a,b], obtaining a function g on [L1, given, construct, algebra] R. Because g is bounded by ∣f∣ on [a,b] and vanishes elsewhere, ∫R∣g(t)∣ dt=∫ab∣f(t)∣ dt<∞, so g∈Lloc1(R). For x∈(a,b) and every r>0, define Er+(x):=[x,x+r),Er−(x):=(x−r,x]. Each family shrinks nicely to x with constant α=12, because Er±(x)⊆B(x,r) and λ(Er±(x))=r=12λ(B(x,r)).

2.1L2step 1.1algebra

Apply [L2] to the set A:=(a,b) and the family Er+(x) from step [L2, step 1.1, algebra] 1.1. This gives a full-measure subset A+⊆(a,b) such that lim⁡r→0+1r∫xx+rg(t) dt=g(x)(x∈A+). Applying [L2] again to the family Er−(x) gives another full-measure subset A−⊆(a,b) such that lim⁡r→0+1r∫x−rxg(t) dt=g(x)(x∈A−). Hence both one-sided limits hold for every x∈A+∩A−, which still has full measure in (a,b). At such an x, if h>0 is small then F(x+h)−F(x)h=1h∫xx+hf(t) dt=1h∫xx+hg(t) dt, while for h<0, F(x+h)−F(x)h=1∣h∣∫x+hxg(t) dt. Both one-sided limits therefore equal g(x)=f(x).

3.1step 2.1givenalgebra∎

Take E=A+∩A− from step 2.1. It is measurable and has full measure in (a,b), and F′(x)=f(x) for every x∈E. If f~=f almost everywhere, then their integrals on every interval [a,x] agree, so they define the same F. Removing also the null set on which their values differ gives F′=f~ on a full-measure set. Thus the conclusion holds for every fixed representative.

Depends on

Dependency tree · 2 levels

Sources