Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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]
- Loading branch information