Theorems · Theorem · measure theory

IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div

∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : 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.

Defined in

Mathlib.MeasureTheory.Covering.DensityTheorem

Cited by

2 results in Mathlib

Foundations

Depth 219 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceMeasurableSpaceIsUnifLocDoublingMeasureSecondCountableTopologyBorelSpaceMeasureTheory.IsLocallyFiniteMeasure