Uniformly locally doubling measures and Lebesgue's density theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

is_unif_loc_doubling_measure.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.

source

@[irreducible]

noncomputable def is_unif_loc_doubling_measure.vitali_family {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] [topological_space.second_countable_topology α] [borel_space α] [measure_theory.is_locally_finite_measure μ] (K : ℝ) :

vitali_family μ

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

Equations

is_unif_loc_doubling_measure.vitali_family μ K = let R : ℝ := is_unif_loc_doubling_measure.scaling_scale_of μ (linear_order.max (4 * K + 3) 3) in (vitali.vitali_family μ (is_unif_loc_doubling_measure.scaling_constant_of μ (linear_order.max (4 * K + 3) 3)) _).enlarge (R / 4) _

source

theorem is_unif_loc_doubling_measure.closed_ball_mem_vitali_family_of_dist_le_mul {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] [topological_space.second_countable_topology α] [borel_space α] [measure_theory.is_locally_finite_measure μ] {K : ℝ} {x y : α} {r : ℝ} (h : has_dist.dist x y ≤ K * r) (rpos : 0 < r) :

metric.closed_ball y r ∈ (is_unif_loc_doubling_measure.vitali_family μ K).sets_at x

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

source

theorem is_unif_loc_doubling_measure.tendsto_closed_ball_filter_at {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] [topological_space.second_countable_topology α] [borel_space α] [measure_theory.is_locally_finite_measure μ] {K : ℝ} {x : α} {ι : Type u_2} {l : filter ι} (w : ι → α) (δ : ι → ℝ) (δlim : filter.tendsto δ l (nhds_within 0 (set.Ioi 0))) (xmem : ∀ᶠ (j : ι) in l, x ∈ metric.closed_ball (w j) (K * δ j)) :

filter.tendsto (λ (j : ι), metric.closed_ball (w j) (δ j)) l ((is_unif_loc_doubling_measure.vitali_family μ K).filter_at x)

source

theorem is_unif_loc_doubling_measure.ae_tendsto_measure_inter_div {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] [topological_space.second_countable_topology α] [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.

source

theorem is_unif_loc_doubling_measure.ae_tendsto_average_norm_sub {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] [topological_space.second_countable_topology α] [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.

source

theorem is_unif_loc_doubling_measure.ae_tendsto_average {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] [topological_space.second_countable_topology α] [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 : ℝ) :

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