# Documentation

Mathlib.MeasureTheory.Covering.DensityTheorem

# Uniformly locally doubling measures and Lebesgue's density theorem #

Lebesgue's density theorem states that given a set S in a sigma compact metric space with locally-finite uniformly locally doubling measure μ then for almost all points x in S, for any sequence of closed balls B₀, B₁, B₂, ... containing x, the limit μ (S ∩ Bⱼ) / μ (Bⱼ) → 1 as j → ∞.

In this file we combine general results about existence of Vitali families for uniformly locally doubling measures with results about differentiation along a Vitali family to obtain an explicit form of Lebesgue's density theorem.

## Main results #

• IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div: a version of Lebesgue's density theorem for sequences of balls converging on a point but whose centres are not required to be fixed.
@[irreducible]
def IsUnifLocDoublingMeasure.vitaliFamily {α : Type u_2} [] [] (μ : ) [] (K : ) :

A Vitali family in a space with a uniformly locally doubling measure, designed so that the sets at x contain all closedBall y r when dist x y ≤ K * r.

Instances For
theorem IsUnifLocDoublingMeasure.vitaliFamily_def {α : Type u_2} [] [] (μ : ) [] (K : ) :
= let R := IsUnifLocDoublingMeasure.scalingScaleOf μ (max (4 * K + 3) 3); let_fun Rpos := (_ : 0 < IsUnifLocDoublingMeasure.scalingScaleOf μ (max (4 * K + 3) 3)); let_fun A := (_ : ∀ (x : α), ∃ᶠ (x_1 : ) in nhdsWithin 0 (), μ (Metric.closedBall x (3 * x_1)) ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ (max (4 * K + 3) 3)) * μ ()); VitaliFamily.enlarge (Vitali.vitaliFamily μ (IsUnifLocDoublingMeasure.scalingConstantOf μ (max (4 * K + 3) 3)) A) (R / 4) (_ : 0 < R / 4)
theorem IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul {α : Type u_1} [] [] (μ : ) [] {K : } {x : α} {y : α} {r : } (h : dist x y K * r) (rpos : 0 < r) :

In the Vitali family IsUnifLocDoublingMeasure.vitaliFamily K, the sets based at x contain all balls closedBall y r when dist x y ≤ K * r.

theorem IsUnifLocDoublingMeasure.tendsto_closedBall_filterAt {α : Type u_1} [] [] (μ : ) [] {K : } {x : α} {ι : Type u_2} {l : } (w : ια) (δ : ι) (δlim : Filter.Tendsto δ l (nhdsWithin 0 ())) (xmem : ∀ᶠ (j : ι) in l, x Metric.closedBall (w j) (K * δ j)) :
Filter.Tendsto (fun j => Metric.closedBall (w j) (δ j)) l ()
theorem IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div {α : Type u_1} [] [] (μ : ) [] (S : Set α) (K : ) :
∀ᵐ (x : α) ∂, ∀ {ι : Type u_3} {l : } (w : ια) (δ : ι), Filter.Tendsto δ l (nhdsWithin 0 ())(∀ᶠ (j : ι) in l, x Metric.closedBall (w j) (K * δ j)) → Filter.Tendsto (fun j => μ (S Metric.closedBall (w j) (δ j)) / μ (Metric.closedBall (w j) (δ j))) l (nhds 1)

A version of Lebesgue's density theorem for a sequence of closed balls whose centers are not required to be fixed.

See also Besicovitch.ae_tendsto_measure_inter_div.

theorem IsUnifLocDoublingMeasure.ae_tendsto_average_norm_sub {α : Type u_1} [] [] (μ : ) [] {E : Type u_2} {f : αE} (hf : ) (K : ) :
∀ᵐ (x : α) ∂μ, ∀ {ι : Type u_3} {l : } (w : ια) (δ : ι), Filter.Tendsto δ l (nhdsWithin 0 ())(∀ᶠ (j : ι) in l, x Metric.closedBall (w j) (K * δ j)) → Filter.Tendsto (fun j => ⨍ (y : α) in Metric.closedBall (w j) (δ j), f y - f xμ) l (nhds 0)

A version of Lebesgue differentiation theorem for a sequence of closed balls whose centers are not required to be fixed.

theorem IsUnifLocDoublingMeasure.ae_tendsto_average {α : Type u_1} [] [] (μ : ) [] {E : Type u_2} [] [] {f : αE} (hf : ) (K : ) :
∀ᵐ (x : α) ∂μ, ∀ {ι : Type u_3} {l : } (w : ια) (δ : ι), Filter.Tendsto δ l (nhdsWithin 0 ())(∀ᶠ (j : ι) in l, x Metric.closedBall (w j) (K * δ j)) → Filter.Tendsto (fun j => ⨍ (y : α) in Metric.closedBall (w j) (δ j), f yμ) l (nhds (f x))

A version of Lebesgue differentiation theorem for a sequence of closed balls whose centers are not required to be fixed.