Theorems · Theorem · measure theory

Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet

∀ {β : Type u} [inst : MetricSpace β] [inst_1 : MeasurableSpace β] [BorelSpace β] [SecondCountableTopology β]
  [HasBesicovitchCovering β] (μ : MeasureTheory.Measure β) [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set β},
  MeasurableSet s →
    ∀ᵐ (x : β) ∂μ,
      Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
        (nhds (s.indicator 1 x))

Given a measurable set s, then μ (s ∩ closedBall x r) / μ (closedBall x r) converges when r tends to 0, for almost every x. The limit is 1 for x ∈ s and 0 for x ∉ s. This shows that almost every point of s is a Lebesgue density point for s. A version for non-measurable sets holds, but it only gives the first conclusion, see ae_tendsto_measure_inter_div.

Defined in

Mathlib.MeasureTheory.Covering.Besicovitch

Cited by

2 results in Mathlib

Foundations

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

Assumes

MetricSpaceMeasurableSpaceBorelSpaceSecondCountableTopologyHasBesicovitchCoveringMeasureTheory.IsLocallyFiniteMeasure