mathlib3 documentation

measure_theory.covering.besicovitch_vector_space

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 #

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

Equations

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

noncomputable def besicovitch.multiplicity (E : Type u_1) [normed_add_comm_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_add_comm_group E] [normed_space E] [finite_dimensional E] (s : finset E) (hs : (c : E), c s c 2) (h : (c : E), c s (d : E), d s c d 1 c - d) :
s.card 5 ^ fdim 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} [normed_add_comm_group E] [normed_space E] [finite_dimensional E] {s : finset E} (hs : (c : E), c s c 2) (h's : (c : E), c s (d : E), d s c d 1 c - d) :
theorem besicovitch.exists_good_δ (E : Type u_1) [normed_add_comm_group E] [normed_space E] [finite_dimensional E] :
(δ : ), 0 < δ δ < 1 (s : finset E), ( (c : E), c s c 2) ( (c : E), c s (d : E), d s c d 1 - δ 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

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.card_le_multiplicity_of_δ {E : Type u_1} [normed_add_comm_group E] [normed_space E] [finite_dimensional E] {s : finset E} (hs : (c : E), c s c 2) (h's : (c : E), c s (d : E), d s c d 1 - besicovitch.good_δ E c - d) :

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_add_comm_group E] {N : } {τ : } (a : besicovitch.satellite_config 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.satellite_config.exists_normalized_aux2 {E : Type u_1} [normed_add_comm_group E] [normed_space E] {N : } {τ : } (a : besicovitch.satellite_config 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.satellite_config.exists_normalized_aux3 {E : Type u_1} [normed_add_comm_group E] [normed_space E] {N : } {τ : } (a : besicovitch.satellite_config 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.satellite_config.exists_normalized {E : Type u_1} [normed_add_comm_group E] [normed_space E] {N : } {τ : } (a : besicovitch.satellite_config 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) (i j : fin N.succ), i j 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.