Commit 2021-10-04 09:48 ab7d2519

feat(measure_theory/covering/besicovitch_vector_space): vector spaces satisfy the assumption of Besicovitch covering theorem (#9461) The Besicovitch covering theorem works in any metric space subject to a technical condition: there should be no satellite configuration of N+1 points, for some N. We prove that this condition is satisfied in finite-dimensional real vector spaces. Moreover, we get the optimal bound for N: it coincides with the maximal number of 1-separated points that fit in a ball of radius 2, by [Füredi and Loeb, On the best constant for the Besicovitch covering theorem][furedi-loeb1994]