mathlib

631f3394 - feat(measure_theory/measure/haar_lebesgue): a density point for closed balls is a density point for rescalings of arbitrary sets (#11620)

feat(measure_theory/measure/haar_lebesgue): a density point for closed balls is a density point for rescalings of arbitrary sets (#11620) Consider a point `x` in a finite-dimensional real vector space with a Haar measure, at which a set `s` has density one, with respect to closed balls (i.e., a Lebesgue density point of `s`). Then `s` has also density one at `x` with respect to any measurable set `t`: the proportion of points in `s` belonging to a rescaled copy `{x} + r • t` of `t` tends to one as `r` tends to zero. In particular, `s ∩ ({x} + r • t)` is nonempty for small enough `r`.