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} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] (K : ℝ) : VitaliFamily μ

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.

Equations

• @IsUnifLocDoublingMeasure.vitaliFamily = IsUnifLocDoublingMeasure.wrapped✝.1

theorem IsUnifLocDoublingMeasure.vitaliFamily_def {α : Type u_2} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] (K : ℝ) : IsUnifLocDoublingMeasure.vitaliFamily μ K = let R := IsUnifLocDoublingMeasure.scalingScaleOf μ (max (4 * K + 3) 3); let_fun Rpos := ⋯; let_fun A := ⋯; VitaliFamily.enlarge (Vitali.vitaliFamily μ (IsUnifLocDoublingMeasure.scalingConstantOf μ (max (4 * K + 3) 3)) A) (R / 4) ⋯

theorem IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {K : ℝ} {x : α} {y : α} {r : ℝ} (h : dist x y ≤ K * r) (rpos : 0 < r) : Metric.closedBall y r ∈ (IsUnifLocDoublingMeasure.vitaliFamily μ K).setsAt x

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} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {K : ℝ} {x : α} {ι : Type u_2} {l : Filter ι} (w : ι → α) (δ : ι → ℝ) (δlim : Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0))) (xmem : ∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) : Filter.Tendsto (fun (j : ι) => Metric.closedBall (w j) (δ j)) l (VitaliFamily.filterAt (IsUnifLocDoublingMeasure.vitaliFamily μ K) x)

theorem IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] (S : Set α) (K : ℝ) : ∀ᵐ (x : α) ∂μ.restrict S, ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 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} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {E : Type u_2} [NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.LocallyIntegrable f μ) (K : ℝ) : ∀ᵐ (x : α) ∂μ, ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 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} [MetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : α → E} (hf : MeasureTheory.LocallyIntegrable f μ) (K : ℝ) : ∀ᵐ (x : α) ∂μ, ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 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.