Satellite configurations for Besicovitch covering lemma in vector spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The Besicovitch covering theorem ensures that, in a nice metric space, there exists a number N such that, from any family of balls with bounded radii, one can extract N families, each made of disjoint balls, covering together all the centers of the initial family.

A key tool in the proof of this theorem is the notion of a satellite configuration, i.e., a family of N + 1 balls, where the first N balls all intersect the last one, but none of them contains the center of another one and their radii are controlled. This is a technical notion, but it shows up naturally in the proof of the Besicovitch theorem (which goes through a greedy algorithm): to ensure that in the end one needs at most N families of balls, the crucial property of the underlying metric space is that there should be no satellite configuration of N + 1 points.

This file is devoted to the study of this property in vector spaces: we prove the main result of Füredi and Loeb, On the best constant for the Besicovitch covering theorem, which shows that the optimal such N in a vector space coincides with the maximal number of points one can put inside the unit ball of radius 2 under the condition that their distances are bounded below by 1. In particular, this number is bounded by 5 ^ dim by a straightforward measure argument.

Main definitions and results #

• multiplicity E is the maximal number of points one can put inside the unit ball of radius 2 in the vector space E, under the condition that their distances are bounded below by 1.
• multiplicity_le E shows that multiplicity E ≤ 5 ^ (dim E).
• good_τ E is a constant > 1, but close enough to 1 that satellite configurations with this parameter τ are not worst than for τ = 1.
• is_empty_satellite_config_multiplicity is the main theorem, saying that there are no satellite configurations of (multiplicity E) + 1 points, for the parameter good_τ E.

Disjoint balls of radius close to 1 in the radius 2 ball. #

Relating satellite configurations to separated points in the ball of radius 2. #

We prove that the number of points in a satellite configuration is bounded by the maximal number of 1-separated points in the ball of radius 2. For this, start from a satellite congifuration c. Without loss of generality, one can assume that the last ball is centered at 0 and of radius 1. Define c' i = c i if ‖c i‖ ≤ 2, and c' i = (2/‖c i‖) • c i if ‖c i‖ > 2. It turns out that these points are 1 - δ-separated, where δ is arbitrarily small if τ is close enough to 1. The number of such configurations is bounded by multiplicity E if δ is suitably small.

To check that the points c' i are 1 - δ-separated, one treats separately the cases where both ‖c i‖ and ‖c j‖ are ≤ 2, where one of them is ≤ 2 and the other one is > 2, and where both of them are > 2.