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, 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 #

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.
Instances For

    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.

    Equations
    Instances For
      theorem Besicovitch.card_le_of_separated {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] (s : Finset E) (hs : cs, c 2) (h : cs, ds, c d1 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.card_le_multiplicity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {s : Finset E} (hs : cs, c 2) (h's : cs, ds, c d1 c - d) :
      theorem Besicovitch.exists_goodδ (E : Type u_1) [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] :
      ∃ (δ : ), 0 < δ δ < 1 ∀ (s : Finset E), (∀ cs, c 2)(∀ cs, ds, c d1 - δ c - d)s.card Besicovitch.multiplicity E

      If δ is small enough, a (1-δ)-separated set in the ball of radius 2 also has cardinality at most multiplicity 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
      Instances For

        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
        Instances For
          theorem Besicovitch.card_le_multiplicity_of_δ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {s : Finset E} (hs : cs, c 2) (h's : cs, ds, c d1 - Besicovitch.goodδ E c - d) :
          theorem Besicovitch.le_multiplicity_of_δ_of_fin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [FiniteDimensional E] {n : } (f : Fin nE) (h : ∀ (i : Fin n), f i 2) (h' : Pairwise fun (i j : Fin n) => 1 - Besicovitch.goodδ E 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} [NormedAddCommGroup E] {N : } {τ : } (a : Besicovitch.SatelliteConfig E N τ) (lastr : a.r (Fin.last N) = 1) (hτ : 1 τ) (δ : ) (hδ1 : τ 1 + δ / 4) (hδ2 : δ 1) (i : Fin N.succ) (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 : Besicovitch.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 : Fin N.succ) (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 : Besicovitch.SatelliteConfig E N τ) (lastc : a.c (Fin.last N) = 0) (lastr : a.r (Fin.last N) = 1) (hτ : 1 τ) (δ : ) (hδ1 : τ 1 + δ / 4) (i : Fin N.succ) (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 : Besicovitch.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.succE), (∀ (n : Fin N.succ), c' n 2) Pairwise fun (i j : Fin N.succ) => 1 - δ 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.