Theorems · Theorem · measure theory

VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet

∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α},
  MeasurableSet s → ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (nhds (s.indicator 1 x))

Given a measurable set s, then μ (s ∩ a) / μ a converges when a shrinks to a typical point x along a Vitali family. 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.Differentiation

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceSecondCountableTopologyBorelSpaceMeasureTheory.IsLocallyFiniteMeasure