mathlib3

84dbe7ba - feat(measure_theory/covering): Lebesgue density points (#11554)

feat(measure_theory/covering): Lebesgue density points (#11554) We show in the general context of differentiation of measures that `μ (s ∩ a) / μ a` converges, when `a` shrinks towards a point `x`, to `1` for almost every `x` in `s`, and to `0` for almost every point outside of `s`. In other words, almost every point of `s` is a Lebesgue density points of `s`. Of course, this requires assumptions on allowed sets `a`. We state this in the general context of Vitali families. We also give easier to use versions in spaces with the Besicovitch property (e.g., final dimensional real vector spaces), where one can take for `a` the closed balls centered at `x`.