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.

Lebesgue differentiation theorem on Rn

Statement

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

Let f∈Lloc1(Rn). Then lim⁡r→0+Arf(x)=f(x) for Lebesgue-almost every x∈Rn.

Facts & Assumptions

Given: The Axiom of Countable Choice and a function f∈Lloc1(Rn).

[L1]

Continuous compactly supported functions are recovered by small ball averages at every point. (Continuous compactly supported functions are recovered by small ball averages)

[L2]

For 1≤p<∞, Cc(Rn) is dense in Lp(Rn). (Cc(Rn) is dense in Lp(Rn) for 1≤p<∞)

[L3]

Chebyshev-Markov controls superlevel sets by the integral. (Chebyshev-Markov inequality for the integral)

[L4]

The centered maximal operator is weak type (1,1). (The centered Hardy-Littlewood maximal operator is weak type (1,1))

[L5]

Under Countable Choice, λn is a complete measure on the Lebesgue sigma-algebra of Rn (Assuming countable choice, L(Rn) is a sigma-algebra containing every elementary set and λn 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 λn-zero sets has measure zero.

Proof

technique · direct
1.1L2givenchooseconstruct

For each integer m≥1 and each integer j≥1, apply [L2] to the [L2, given, choose, construct] L1 function f1B(0,m+1) and choose gm,j∈Cc(Rn) such that ∫B(0,m+1)∣f−gm,j∣ dλ<2−2j5n. Set hm,j:=(f−gm,j)1B(0,m+1).

2.1L3L4L5step 1.1algebra

Let [L3, L4, L5, step 1.1, algebra] Em,j:={x∈B(0,m):Mhm,j(x)>2−j}∪{x∈B(0,m):∣hm,j(x)∣>2−j}. Both sets are Lebesgue measurable: the maximal superlevel set is open by the ball-average continuity argument in [L4], and hm,j is measurable. Finite subadditivity [L5], [L4] and [L3] give λ(Em,j)≤5n2−j∥hm,j∥1+12−j∥hm,j∥1<2−j+5−n2−j≤21−j.

3.1L5step 2.1algebra

For fixed m, put [step 2.1, algebra] Nm:=⋂N=1∞⋃j≥NEm,j. The sets Em,j, their countable unions, and Nm are measurable by [L5]. By countable subadditivity [L5] and step 2.1 λ ⁣(⋃j≥NEm,j)≤∑j≥Nλ(Em,j)≤∑j≥N21−j=22−N. For every N, inclusion and monotonicity [L5] give 0≤λ(Nm)≤22−N. Given ϵ>0, choose N with 22−N<ϵ; thus λ(Nm)=0. This uses small positive tail measures, without asserting that any Em,j is null.

4.1L1step 1.1step 3.1algebra

Let x∈B(0,m)∖Nm. Then there is Nx such that [L1, step 1.1, step 3.1, algebra] x∉Em,j for every j≥Nx. Fix such a j and take 0<r<1. Since x∈B(0,m), one has B(x,r)⊆B(0,m+1), so Arf(x)−f(x)=(Argm,j(x)−gm,j(x))+Arhm,j(x)−hm,j(x). Therefore ∣Arf(x)−f(x)∣≤∣Argm,j(x)−gm,j(x)∣+Mhm,j(x)+∣hm,j(x)∣≤∣Argm,j(x)−gm,j(x)∣+21−j. Now [L1] gives Argm,j(x)→gm,j(x), so lim sup⁡r→0+∣Arf(x)−f(x)∣≤21−j for every j≥Nx. Letting j→∞ yields Arf(x)→f(x).

5.1step 3.1step 4.1L5∎

The bad set for radius differentiation is contained in [step 3.1, step 4.1, L5] ⋃m≥1Nm, which is null by [L5]. Thus the convergence holds for almost every x∈Rn.

Depends on

Used by

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