# mathlibdocumentation

measure_theory.covering.besicovitch_vector_space

# Satellite configurations for Besicovitch covering lemma in vector spaces #

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.
noncomputable def besicovitch.satellite_config.center_and_rescale {E : Type u_1} [normed_group E] [ E] {N : } {τ : } (a : τ) :

Rescaling a satellite configuration in a vector space, to put the basepoint at 0 and the base radius at 1.

Equations
theorem besicovitch.satellite_config.center_and_rescale_center {E : Type u_1} [normed_group E] [ E] {N : } {τ : } (a : τ) :
theorem besicovitch.satellite_config.center_and_rescale_radius {E : Type u_1} [normed_group E] [ E] {N : } {τ : } (a : τ) :

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

noncomputable def besicovitch.multiplicity (E : Type u_1) [normed_group E] :

The maximum cardinality of a 1-separated set in the ball of radius 2. This is also the optimal number of families in the Besicovitch covering theorem.

Equations
theorem besicovitch.card_le_of_separated {E : Type u_1} [normed_group E] [ E] (s : finset E) (hs : ∀ (c : E), c sc 2) (h : ∀ (c : E), c s∀ (d : E), d sc d1 c - d) :

Any 1-separated set in the ball of radius 2 has cardinality at most 5 ^ dim. This is useful to show that the supremum in the definition of besicovitch.multiplicity E is well behaved.

theorem besicovitch.multiplicity_le {E : Type u_1} [normed_group E] [ E]  :
theorem besicovitch.card_le_multiplicity {E : Type u_1} [normed_group E] [ E] {s : finset E} (hs : ∀ (c : E), c sc 2) (h's : ∀ (c : E), c s∀ (d : E), d sc d1 c - d) :
theorem besicovitch.exists_good_δ (E : Type u_1) [normed_group E] [ E]  :
∃ (δ : ), 0 < δ δ < 1 ∀ (s : finset E), (∀ (c : E), c sc 2)(∀ (c : E), c s∀ (d : E), d sc d1 - δ c - d)

If δ is small enough, a (1-δ)-separated set in the ball of radius 2 also has cardinality at most multiplicity E.

noncomputable def besicovitch.good_δ (E : Type u_1) [normed_group E] [ E]  :

A small positive number such that any 1 - δ-separated set in the ball of radius 2 has cardinality at most besicovitch.multiplicity E.

Equations
theorem besicovitch.good_δ_lt_one (E : Type u_1) [normed_group E] [ E]  :
noncomputable def besicovitch.good_τ (E : Type u_1) [normed_group E] [ E]  :

A number τ > 1, but chosen close enough to 1 so that the construction in the Besicovitch covering theorem using this parameter τ will give the smallest possible number of covering families.

Equations
theorem besicovitch.one_lt_good_τ (E : Type u_1) [normed_group E] [ E]  :
theorem besicovitch.card_le_multiplicity_of_δ {E : Type u_1} [normed_group E] [ E] {s : finset E} (hs : ∀ (c : E), c sc 2) (h's : ∀ (c : E), c s∀ (d : E), d sc d c - d) :
theorem besicovitch.le_multiplicity_of_δ_of_fin {E : Type u_1} [normed_group E] [ E] {n : } (f : fin n → E) (h : ∀ (i : fin n), f i 2) (h' : ∀ (i j : fin n), i j f i - f j) :

### 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`.

theorem besicovitch.satellite_config.exists_normalized_aux1 {E : Type u_1} [normed_group E] {N : } {τ : } (a : τ) (lastr : a.r (fin.last N) = 1) (hτ : 1 τ) (δ : ) (hδ1 : τ 1 + δ / 4) (hδ2 : δ 1) (i j : fin N.succ) (inej : i j) :
1 - δ a.c i - a.c j
theorem besicovitch.satellite_config.exists_normalized_aux2 {E : Type u_1} [normed_group E] [ E] {N : } {τ : } (a : τ) (lastc : a.c (fin.last N) = 0) (lastr : a.r (fin.last N) = 1) (hτ : 1 τ) (δ : ) (hδ1 : τ 1 + δ / 4) (hδ2 : δ 1) (i j : fin N.succ) (inej : i j) (hi : a.c i 2) (hj : 2 < a.c j) :
1 - δ a.c i - (2 / a.c j) a.c j
theorem besicovitch.satellite_config.exists_normalized_aux3 {E : Type u_1} [normed_group E] [ E] {N : } {τ : } (a : τ) (lastc : a.c (fin.last N) = 0) (lastr : a.r (fin.last N) = 1) (hτ : 1 τ) (δ : ) (hδ1 : τ 1 + δ / 4) (i j : fin N.succ) (inej : i j) (hi : 2 < a.c i) (hij : a.c i a.c j) :
1 - δ (2 / a.c i) a.c i - (2 / a.c j) a.c j
theorem besicovitch.satellite_config.exists_normalized {E : Type u_1} [normed_group E] [ E] {N : } {τ : } (a : τ) (lastc : a.c (fin.last N) = 0) (lastr : a.r (fin.last N) = 1) (hτ : 1 τ) (δ : ) (hδ1 : τ 1 + δ / 4) (hδ2 : δ 1) :
∃ (c' : fin N.succ → E), (∀ (n : fin N.succ), c' n 2) ∀ (i j : fin N.succ), i j1 - δ c' i - c' j

In a normed vector space E, there can be no satellite configuration with multiplicity E + 1 points and the parameter good_τ E. This will ensure that in the inductive construction to get the Besicovitch covering families, there will never be more than multiplicity E nonempty families.

@[protected, instance]
def besicovitch.has_besicovitch_covering (E : Type u_1) [normed_group E] [ E]  :