Theorems · Theorem · measure theory

VitaliFamily.ae_tendsto_measure_inter_div

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

Given an arbitrary set s, then μ (s ∩ a) / μ a converges to 1 when a shrinks to a typical point of s along a Vitali family. This shows that almost every point of s is a Lebesgue density point for s. A stronger version for measurable sets is given in ae_tendsto_measure_inter_div_of_measurableSet.

Defined in

Mathlib.MeasureTheory.Covering.Differentiation

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceSecondCountableTopologyBorelSpaceMeasureTheory.IsLocallyFiniteMeasure