TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-04

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.

Almost every point is a Lebesgue point of a locally integrable function

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Let $f \in L_{l o c}^{1} (R^{n})$ . Then the Lebesgue set of the $L_{l o c}^{1}$ class of $f$ has full Lebesgue measure.

Equivalently, for almost every $x \in R^{n}$ , $\lim_{r \to 0^{+}} \frac{1}{λ (B (x, r))} \int_{B (x, r)} ∣ f (y) - f (x) ∣ d λ (y) = 0.$

Facts & Assumptions

Given: The Axiom of Countable Choice and a locally integrable function $f$ on $R^{n}$ .

[L1]

A point belongs to the Lebesgue set exactly when the averaged oscillation above tends to $0$ . (Lebesgue points and the Lebesgue set of an $L_{l o c}^{1}$ class)

[L2]

A property holds almost everywhere when its exceptional set is contained in a measurable null set. (Measure-null sets and almost-everywhere statements relative to a measure)

[L3]

The rationals are countably infinite, and the product of two at most countable sets is at most countable. ( $Q$ is countably infinite, A product of two at most countable sets is at most countable)

[L4]

Rationals are dense in the reals. (The rationals embed densely in the reals)

[L5]

A countable union of null sets is null. (A countable union of measure-zero sets has measure zero, by countable choice)

[L6]

If $u \in L_{l o c}^{1} (R^{n})$ , then $A_{r} u (x) \to u (x)$ for almost every $x$ . (Lebesgue differentiation theorem on $R^{n}$ )

Proof

technique · direct

1.1

Let [L3, L5, L6, given, construct] $D : = {a + i b : a, b \in Q} .$ By [L3], $D$ is countable. For each $c \in D$ , the function $u_{c} : = ∣ f - c ∣$ is locally integrable, so [L6] gives a null set $N_{c}$ such that $\lim_{r \to 0^{+}} A_{r} u_{c} (x) = u_{c} (x) = ∣ f (x) - c ∣$ for every $x \notin N_{c}$ . Put $N : = ⋃_{c \in D} N_{c} .$ By [L5], $N$ is null.

L3L5L6givenconstruct

2.1

Fix $x \notin N$ and let $ε > 0$ . By density [L4], choose [step 1.1, L4, algebra] $c \in D$ with $∣ f (x) - c ∣ < ε$ . Then for every $r > 0$ , $\frac{1}{λ (B (x, r))} \int_{B (x, r)} ∣ f (y) - f (x) ∣ d λ (y) \leq A_{r} ∣ f - c ∣ (x) + ∣ c - f (x) ∣ .$ Taking $r \to 0^{+}$ and using step 1.1 gives ${lim sup}_{r \to 0^{+}} \frac{1}{λ (B (x, r))} \int_{B (x, r)} ∣ f (y) - f (x) ∣ d λ (y) \leq 2 ε .$ Since $ε$ is arbitrary, the limit is $0$ .

step 1.1L4algebra

3.1

Step 2.1 holds for every $x \notin N$ , and $N$ is null. By [L1] and [L2], [L1, L2, step 1.1, step 2.1] the Lebesgue set of the class of $f$ has full measure.

L1L2step 1.1step 2.1∎

Depends on

Used by

Differentiation holds along families shrinking nicely Theorem
Lebesgue density theorem Theorem

Dependency tree · two levels

57 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

Gerald B. Folland, Real Analysis: Modern Techniques and Their Applications, 2nd ed., Theorem 3.20 (standard reference, not scraped)
Walter Rudin, Real and Complex Analysis, 3rd ed., Theorem 7.7 (standard reference, not scraped)