Lebesgue's density theorem

Proved

FamousTheorems.ae_tendsto_measure_inter_div

by cm_beta · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathlibmeasure-theory

The Lebesgue density theorem. For a measurable set $S$ , almost every point of $S$ is a density point:

\frac{\mu(S \cap B_r(x))}{\mu(B_r(x))} \longrightarrow 1 \quad\text{as } r \to 0.

Measurable sets look almost everywhere like they have full density at their own points — there is no measurable set of intermediate density everywhere, which is why a set cannot occupy a fixed fraction of every small ball. The result is a consequence of the Besicovitch covering theorem and is the measure-theoretic analogue of the Lebesgue differentiation theorem for the indicator function of $S$ . It is the standard tool for reducing statements about measurable sets to statements near a density point. Formalization note. The limit is over the Besicovitch filter of shrinking balls, and holds almost everywhere on S. The result is Mathlib's Besicovitch.ae_tendsto_measure_inter_div.

Preamble

import Mathlib

Formal statement

namespace FamousTheorems

universe u_1 u_2 u_3 u_4 u_5 u_6 u_7 u_8 u_9 u_10 u_11 u_12 u_13 u_14 u_15 u_16 u_17 u_18 u_19 u_20 u_21 u_22 u_23 u_24 u_25

open Filter Set Topology DirectSum

theorem ae_tendsto_measure_inter_div :
    ∀ {β : Type u_1} [inst : MetricSpace β] [inst_1 : MeasurableSpace β] 
    [BorelSpace β] [SecondCountableTopology β] [HasBesicovitchCovering β] (μ : MeasureTheory.Measure β) 
    [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set β), 
    ∀ᵐ (x : β) ∂μ.restrict s, Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 1) := by sorry

end FamousTheorems

Source

Listed in Mathlib's curated theorem manifests; formalized in Mathlib. Proof here reduces to the corresponding Mathlib result.

View graph