Lebesgue Density Theorem

Stream: Is there code for X?

[Yaël Dillies]

Jason, Bhavik and I are proving that order-connected sets are measurable. For this we need the Lebesgue Density Theorem. Is it somewhere in mathlib?

[Yaël Dillies]

Ahah! It looks like it is docs#vitali_family.ae_tendsto_measure_inter_div_of_measurable_set

[Jason KY.]

Also Yael found out we also have docs#set.ord_connected.measurable_set already!

[Oliver Nash]

I need a version of the Lebesgue Density Theorem with a sequence of balls whose centres are not fixed.

A month or so ago I cobbled together the following which is sufficient for my purposes (in my application α is just the circle):

import measure_theory.covering.vitali
import measure_theory.covering.differentiation

open set filter function metric measure_theory measure_theory.measure_space
open_locale nnreal ennreal topological_space

variables {α : Type*} [measurable_space α] (μ : measure α)
variables [metric_space α] [proper_space α] [borel_space α] [is_locally_finite_measure μ]

lemma closed_ball.ae_tendsto_measure_inter_div
  (f : ℝ≥0 → ℝ≥0) (d : ℝ)
  (hfd : ∀ (t : ℝ≥0), ∀ᶠ (ε : ℝ≥0) in 𝓝 0, f (t * ε) = t^d * f ε)
  (hfμ : ∀ᶠ (ε : ℝ≥0) in 𝓝 0, ∀ x, μ (closed_ball x ε) = f ε)
  (S : set α) :
  ∀ᵐ x ∂μ.restrict S, ∀ (w : ℕ → α) (δ : ℕ → ℝ)
    (hδ₀ : ∀ j, 0 < δ j)
    (hδ₁ : tendsto δ at_top (𝓝 0))
    (hδ₂ : ∀ j, x ∈ closed_ball (w j) (δ j)),
    tendsto (λ j, μ (S ∩ closed_ball (w j) (δ j)) / μ (closed_ball (w j) (δ j))) at_top (𝓝 1) :=
sorry -- I have a (horrible) proof of this.

but I would like to get the statement set down in the appropriate generality and I am not happy with the above.

At first I thought that the assumptions of docs#besicovitch.ae_tendsto_measure_inter_div might be sufficient but now I am not so sure. I know nothing of Besicovitch theory!

Can some measure theorist point me in the right direction?

[Sebastien Gouezel]

The right assumption is probably to assume that the ratio of measures mu (B(x, 2 r)) / mu (B (x, r)) is uniformly bounded. (More precisely, it is enough to assume that there exists C such that, for all x, for all small enough r, then mu (B(x, 2r)) ≤ C * mu (B(x, r))).

I don't know how your proof looks, but to me it looks like all the math is already in ae_tendsto_measure_inter_div, and that you just need a little bit of glue to apply it in your context. Here is a possible skeleton:

import measure_theory.covering.vitali
import measure_theory.covering.differentiation

open set filter function metric measure_theory measure_theory.measure_space
open_locale nnreal ennreal topological_space

variables {α : Type*} [measurable_space α] {μ : measure α}
variables [metric_space α] [proper_space α] [borel_space α] [is_locally_finite_measure μ]

lemma vitali_family.tendsto_filter_at (v : vitali_family μ) {β : Type*} {l : filter β}
  {f : β → set α} {x : α}
  (H : ∀ᶠ i in l, f i ∈ v.sets_at x) (H' : ∀ (ε > (0 : ℝ)), ∀ᶠ i in l, f i ⊆ closed_ball x ε) :
  tendsto f l (v.filter_at x)  :=
begin
  assume s hs,
  change ∀ᶠ i in l, f i ∈ s,
  obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ) (H : ε > 0), ∀ (a : set α),
    a ∈ v.sets_at x → a ⊆ closed_ball x ε → a ∈ s :=
      (vitali_family.mem_filter_at_iff _).1 hs,
  filter_upwards [H, H' ε εpos] with i hi h'i using hε _ hi h'i,
end

lemma closed_ball.ae_tendsto_measure_inter_div
  (f : ℝ≥0 → ℝ≥0) (d : ℝ)
  (hfd : ∀ (t : ℝ≥0), ∀ᶠ (ε : ℝ≥0) in 𝓝 0, f (t * ε) = t^d * f ε)
  (hfμ : ∀ᶠ (ε : ℝ≥0) in 𝓝 0, ∀ x, μ (closed_ball x ε) = f ε)
  (S : set α) :
  ∀ᵐ x ∂μ.restrict S, ∀ (w : ℕ → α) (δ : ℕ → ℝ)
    (hδ₀ : ∀ j, 0 < δ j)
    (hδ₁ : tendsto δ at_top (𝓝 0))
    (hδ₂ : ∀ j, x ∈ closed_ball (w j) (δ j)),
    tendsto (λ j, μ (S ∩ closed_ball (w j) (δ j)) / μ (closed_ball (w j) (δ j))) at_top (𝓝 1) :=
begin
  let v : vitali_family μ := vitali.vitali_family μ (6^d) sorry,
  filter_upwards [v.ae_tendsto_measure_inter_div S] with x hx,
  assume w δ δpos δlim xmem,
  have : tendsto (λ j, closed_ball (w j) (δ j)) at_top (v.filter_at x),
  { apply v.tendsto_filter_at,
    { simp only [v, vitali.vitali_family, mem_set_of_eq, mem_closed_ball],
      sorry },
    { sorry } },
  exact hx.comp this,
end

(the lemma vitali_family.tendsto_filter_at is clearly missing in the current API, and it should probably be formulated as an iff).

[Oliver Nash]

Thank you very much @Sebastien Gouezel If I'm lucky I'll have time to take this up this afternoon (but it might not be till next week). I'll report back when I do!

[Oliver Nash]

I have finally returned to this and created a PR: #16762