Theorems · Theorem · measure theory

Besicovitch.ae_tendsto_measure_inter_div

• 1000+ list: Lebesgue's density theorem

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

Given an arbitrary set s, then μ (s ∩ closedBall x r) / μ (closedBall x r) converges to 1 when r tends to 0, for almost every x in s. This shows that almost every point of s is a Lebesgue density point for s. A stronger version holds for measurable sets, see ae_tendsto_measure_inter_div_of_measurableSet. See also IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div.

Defined in

Mathlib.MeasureTheory.Covering.Besicovitch

Cited by

1 results in Mathlib

Foundations

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

Assumes

MetricSpaceMeasurableSpaceBorelSpaceSecondCountableTopologyHasBesicovitchCoveringMeasureTheory.IsLocallyFiniteMeasure