mathlib documentation

measure_theory.covering.density_theorem

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 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 doubling measures with results about differentiation along a Vitali family to obtain an explicit form of Lebesgue's density theorem.

Main results #

@[irreducible]

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

Equations

In the Vitali family is_doubling_measure.vitali_family K, the sets based at x contain all balls closed_ball y r when dist x y ≤ K * r.

theorem is_doubling_measure.ae_tendsto_measure_inter_div {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_doubling_measure μ] [sigma_compact_space α] [borel_space α] [measure_theory.is_locally_finite_measure μ] (S : set α) (K : ) :
∀ᵐ (x : α) μ.restrict S, {ι : Type u_2} {l : filter ι} (w : ι α) (δ : ι ), filter.tendsto δ l (nhds_within 0 (set.Ioi 0)) (∀ᶠ (j : ι) in l, x metric.closed_ball (w j) (K * δ j)) filter.tendsto (λ (j : ι), μ (S metric.closed_ball (w j) (δ j)) / μ (metric.closed_ball (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 is_doubling_measure.ae_tendsto_average_norm_sub {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_doubling_measure μ] [sigma_compact_space α] [borel_space α] [measure_theory.is_locally_finite_measure μ] {E : Type u_2} [normed_add_comm_group E] {f : α E} (hf : measure_theory.integrable f μ) (K : ) :
∀ᵐ (x : α) μ, {ι : Type u_3} {l : filter ι} (w : ι α) (δ : ι ), filter.tendsto δ l (nhds_within 0 (set.Ioi 0)) (∀ᶠ (j : ι) in l, x metric.closed_ball (w j) (K * δ j)) filter.tendsto (λ (j : ι), (y : α) in metric.closed_ball (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 is_doubling_measure.ae_tendsto_average {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_doubling_measure μ] [sigma_compact_space α] [borel_space α] [measure_theory.is_locally_finite_measure μ] {E : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] {f : α E} (hf : measure_theory.integrable f μ) (K : ) :
∀ᵐ (x : α) μ, {ι : Type u_3} {l : filter ι} (w : ι α) (δ : ι ), filter.tendsto δ l (nhds_within 0 (set.Ioi 0)) (∀ᶠ (j : ι) in l, x metric.closed_ball (w j) (K * δ j)) filter.tendsto (λ (j : ι), (y : α) in metric.closed_ball (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.