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} [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) : SatelliteConfig E N τ

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

Equations

• One or more equations did not get rendered due to their size.

theorem Besicovitch.SatelliteConfig.centerAndRescale_center {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) : a.centerAndRescale.c (Fin.last N) = 0

theorem Besicovitch.SatelliteConfig.centerAndRescale_radius {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) : a.centerAndRescale.r (Fin.last N) = 1

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

def Besicovitch.multiplicity (E : Type u_2) [NormedAddCommGroup 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

• Besicovitch.multiplicity E = sSup {N : ℕ | ∃ (s : Finset E), s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}

theorem Besicovitch.card_le_of_separated {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Finset E) (hs : ∀ c ∈ s, ‖c‖ ≤ 2) (h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖) : s.card ≤ 5 ^ Module.finrank ℝ E

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} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : multiplicity E ≤ 5 ^ Module.finrank ℝ E

theorem Besicovitch.card_le_multiplicity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Finset E} (hs : ∀ c ∈ s, ‖c‖ ≤ 2) (h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖) : s.card ≤ multiplicity E

theorem Besicovitch.exists_goodδ (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : ∃ (δ : ℝ), 0 < δ ∧ δ < 1 ∧ ∀ (s : Finset E), (∀ c ∈ s, ‖c‖ ≤ 2) → (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) → s.card ≤ multiplicity E

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) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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

• Besicovitch.goodδ E = ⋯.choose

theorem Besicovitch.goodδ_lt_one (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : goodδ E < 1

def Besicovitch.goodτ (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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

• Besicovitch.goodτ E = 1 + Besicovitch.goodδ E / 4

theorem Besicovitch.one_lt_goodτ (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : 1 < goodτ E

theorem Besicovitch.card_le_multiplicity_of_δ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Finset E} (hs : ∀ c ∈ s, ‖c‖ ≤ 2) (h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - goodδ E ≤ ‖c - d‖) : s.card ≤ multiplicity E

theorem Besicovitch.le_multiplicity_of_δ_of_fin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (f : Fin n → E) (h : ∀ (i : Fin n), ‖f i‖ ≤ 2) (h' : Pairwise fun (i j : Fin n) => 1 - goodδ E ≤ ‖f i - f j‖) : n ≤ multiplicity E

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} [NormedAddCommGroup E] {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) (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.SatelliteConfig.exists_normalized_aux2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) (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.SatelliteConfig.exists_normalized_aux3 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) (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.SatelliteConfig.exists_normalized {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ) (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) ∧ Pairwise fun (i j : Fin N.succ) => 1 - δ ≤ ‖c' i - c' j‖

theorem Besicovitch.isEmpty_satelliteConfig_multiplicity (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : IsEmpty (SatelliteConfig E (multiplicity E) (goodτ E))

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.

@[instance 100]

instance Besicovitch.instHasBesicovitchCovering (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : HasBesicovitchCovering E