# Documentation

Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

# 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][furedi-loeb1994], 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.
• isEmpty_satelliteConfig_multiplicity is the main theorem, saying that there are no satellite configurations of (multiplicity E) + 1 points, for the parameter goodτ E.
def Besicovitch.SatelliteConfig.centerAndRescale {E : Type u_1} [] {N : } {τ : } (a : ) :

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

Instances For
theorem Besicovitch.SatelliteConfig.centerAndRescale_center {E : Type u_1} [] {N : } {τ : } (a : ) :
theorem Besicovitch.SatelliteConfig.centerAndRescale_radius {E : Type u_1} [] {N : } {τ : } (a : ) :

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

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.

Instances For
theorem Besicovitch.card_le_of_separated {E : Type u_1} [] [] (s : ) (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} [] [] :
theorem Besicovitch.card_le_multiplicity {E : Type u_1} [] [] {s : } (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) [] [] :
δ, 0 < δ δ < 1 ∀ (s : ), (∀ (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.

def Besicovitch.goodδ (E : Type u_1) [] [] :

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

Instances For
theorem Besicovitch.goodδ_lt_one (E : Type u_1) [] [] :
def Besicovitch.goodτ (E : Type u_1) [] [] :

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.

Instances For
theorem Besicovitch.one_lt_goodτ (E : Type u_1) [] [] :
theorem Besicovitch.card_le_multiplicity_of_δ {E : Type u_1} [] [] {s : } (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} [] [] {n : } (f : Fin nE) (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 configuration 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.SatelliteConfig.exists_normalized_aux1 {E : Type u_1} {N : } {τ : } (a : ) (lastr : ) (hτ : 1 τ) (δ : ) (hδ1 : τ 1 + δ / 4) (hδ2 : δ 1) (i : Fin ()) (j : Fin ()) (inej : i j) :
theorem Besicovitch.SatelliteConfig.exists_normalized_aux2 {E : Type u_1} [] {N : } {τ : } (a : ) (lastc : ) (lastr : ) (hτ : 1 τ) (δ : ) (hδ1 : τ 1 + δ / 4) (hδ2 : δ 1) (i : Fin ()) (j : Fin ()) (inej : i j) (hi : ) (hj : ) :
1 - δ
theorem Besicovitch.SatelliteConfig.exists_normalized_aux3 {E : Type u_1} [] {N : } {τ : } (a : ) (lastc : ) (lastr : ) (hτ : 1 τ) (δ : ) (hδ1 : τ 1 + δ / 4) (i : Fin ()) (j : Fin ()) (inej : i j) (hi : ) (hij : ) :
1 - δ
theorem Besicovitch.SatelliteConfig.exists_normalized {E : Type u_1} [] {N : } {τ : } (a : ) (lastc : ) (lastr : ) (hτ : 1 τ) (δ : ) (hδ1 : τ 1 + δ / 4) (hδ2 : δ 1) :
c', (∀ (n : Fin ()), c' n 2) ∀ (i j : Fin ()), 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.