# mathlibdocumentation

measure_theory.covering.besicovitch

# Besicovitch covering theorems #

The topological 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.

By "nice metric space", we mean a technical property stated as follows: there exists no satellite configuration of N+1 points (with a given parameter τ > 1). Such a configuration is 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 property is for instance satisfied by finite-dimensional real vector spaces.

In this file, we prove the topological Besicovitch covering theorem, in besicovitch.exist_disjoint_covering_families.

The measurable Besicovitch theorem ensures that, in the same class of metric spaces, if at every point one considers a class of balls of arbitrarily small radii, called admissible balls, then one can cover almost all the space by a family of disjoint admissible balls. It is deduced from the topological Besicovitch theorem, and proved in besicovitch.exists_disjoint_closed_ball_covering_ae.

## Main definitions and results #

• satellite_config α N τ is the type of all satellite configurations of N+1 points in the metric space α, with parameter τ.
• has_besicovitch_covering is a class recording that there exist N and τ > 1 such that there is no satellite configuration of N+1 points with parameter τ.
• exist_disjoint_covering_families is the topological Besicovitch covering theorem: from any family of balls one can extract finitely many disjoint subfamilies covering the same set.
• exists_disjoint_closed_ball_covering is the measurable Besicovitch covering theorem: from any family of balls with arbitrarily small radii at every point, one can extract countably many disjoint balls covering almost all the space. While the value of N is relevant for the precise statement of the topological Besicovitch theorem, it becomes irrelevant for the measurable one. Therefore, this statement is expressed using the Prop-valued typeclass has_besicovitch_covering.

## Implementation #

#### Sketch of proof of the topological Besicovitch theorem: #

We choose balls in a greedy way. First choose a ball with maximal radius (or rather, since there is no guarantee the maximal radius is realized, a ball with radius within a factor τ of the supremum). Then, remove all balls whose center is covered by the first ball, and choose among the remaining ones a ball with radius close to maximum. Go on forever until there is no available center (this is a transfinite induction in general).

Then define inductively a coloring of the balls. A ball will be of color i if it intersects already chosen balls of color 0, ..., i - 1, but none of color i. In this way, balls of the same color form a disjoint family, and the space is covered by the families of the different colors.

The nontrivial part is to show that at most N colors are used. If one needs N+1 colors, consider the first time this happens. Then the corresponding ball intersects N balls of the different colors. Moreover, the inductive construction ensures that the radii of all the balls are controlled: they form a satellite configuration with N+1 balls (essentially by definition of satellite configurations). Since we assume that there are no such configurations, this is a contradiction.

#### Sketch of proof of the measurable Besicovitch theorem: #

From the topological Besicovitch theorem, one can find a disjoint countable family of balls covering a proportion > 1/(N+1) of the space. Taking a large enough finite subset of these balls, one gets the same property for finitely many balls. Their union is closed. Therefore, any point in the complement has around it an admissible ball not intersecting these finitely many balls. Applying again the topological Besicovitch theorem, one extracts from these a disjoint countable subfamily covering a proportion > 1/(N+1) of the remaining points, and then even a disjoint finite subfamily. Then one goes on again and again, covering at each step a positive proportion of the remaining points, while remaining disjoint from the already chosen balls. The union of all these balls is the desired almost everywhere covering.

### Satellite configurations #

structure besicovitch.satellite_config (α : Type u_1) [metric_space α] (N : ) (τ : ) :
Type u_1

A satellite configuration is a configuration of N+1 points that shows up in the inductive construction for the Besicovitch covering theorem. It depends on some parameter τ ≥ 1.

This is a family of balls (indexed by i : fin N.succ, with center c i and radius r i) such that the last ball intersects all the other balls (condition inter), and given any two balls there is an order between them, ensuring that the first ball does not contain the center of the other one, and the radius of the second ball can not be larger than the radius of the first ball (up to a factor τ). This order corresponds to the order of choice in the inductive construction: otherwise, the second ball would have been chosen before. This is the condition h.

Finally, the last ball is chosen after all the other ones, meaning that h can be strengthened by keeping only one side of the alternative in hlast.

@[class]
structure has_besicovitch_covering (α : Type u_1) [metric_space α] :
Prop
• no_satellite_config : ∃ (N : ) (τ : ), 1 < τ

A metric space has the Besicovitch covering property if there exist N and τ > 1 such that there are no satellite configuration of parameter τ with N+1 points. This is the condition that guarantees that the measurable Besicovitch covering theorem holds. It is satified by finite-dimensional real vector spaces.

Instances
@[protected, instance]
def besicovitch.satellite_config.inhabited {α : Type u_1} {τ : } [inhabited α] [metric_space α] :

There is always a satellite configuration with a single point.

Equations
theorem besicovitch.satellite_config.inter' {α : Type u_1} [metric_space α] {N : } {τ : } (a : τ) (i : fin N.succ) :
dist (a.c i) (a.c (fin.last N)) a.r i + a.r (fin.last N)
theorem besicovitch.satellite_config.hlast' {α : Type u_1} [metric_space α] {N : } {τ : } (a : τ) (i : fin N.succ) (h : 1 τ) :
a.r (fin.last N) τ * a.r i

### Extracting disjoint subfamilies from a ball covering #

structure besicovitch.ball_package (β : Type u_1) (α : Type u_2) :
Type (max u_1 u_2)
• c : β → α
• r : β →
• rpos : ∀ (b : β), 0 < self.r b
• r_bound :
• r_le : ∀ (b : β), self.r b self.r_bound

A ball package is a family of balls in a metric space with positive bounded radii.

def besicovitch.unit_ball_package (α : Type u_1) :

The ball package made of unit balls.

Equations
@[protected, instance]
def besicovitch.ball_package.inhabited (α : Type u_1) :
Equations
structure besicovitch.tau_package (β : Type u_1) (α : Type u_2) :
Type (max u_1 u_2)
• to_ball_package :
• τ :
• one_lt_tau : 1 < self.τ

A Besicovitch tau-package is a family of balls in a metric space with positive bounded radii, together with enough data to proceed with the Besicovitch greedy algorithm. We register this in a single structure to make sure that all our constructions in this algorithm only depend on one variable.

@[protected, instance]
def besicovitch.tau_package.inhabited (α : Type u_1) :
Equations
noncomputable def besicovitch.tau_package.index {α : Type u_1} [metric_space α] {β : Type u} [nonempty β] (p : α) :
ordinal → β

Choose inductively large balls with centers that are not contained in the union of already chosen balls. This is a transfinite induction.

Equations
def besicovitch.tau_package.Union_up_to {α : Type u_1} [metric_space α] {β : Type u} [nonempty β] (p : α) (i : ordinal) :
set α

The set of points that are covered by the union of balls selected at steps < i.

Equations
theorem besicovitch.tau_package.monotone_Union_up_to {α : Type u_1} [metric_space α] {β : Type u} [nonempty β] (p : α) :
noncomputable def besicovitch.tau_package.R {α : Type u_1} [metric_space α] {β : Type u} [nonempty β] (p : α) (i : ordinal) :

Supremum of the radii of balls whose centers are not yet covered at step i.

Equations
noncomputable def besicovitch.tau_package.color {α : Type u_1} [metric_space α] {β : Type u} [nonempty β] (p : α) :

Group the balls into disjoint families, by assigning to a ball the smallest color for which it does not intersect any already chosen ball of this color.

Equations
noncomputable def besicovitch.tau_package.last_step {α : Type u_1} [metric_space α] {β : Type u} [nonempty β] (p : α) :

p.last_step is the first ordinal where the construction stops making sense, i.e., f returns garbage since there is no point left to be chosen. We will only use ordinals before this step.

Equations
theorem besicovitch.tau_package.last_step_nonempty {α : Type u_1} [metric_space α] {β : Type u} [nonempty β] (p : α) :
{i : ordinal | ¬∃ (b : β), p.to_ball_package.c b p.Union_up_to i p.R i (p.τ) * p.to_ball_package.r b}.nonempty
theorem besicovitch.tau_package.mem_Union_up_to_last_step {α : Type u_1} [metric_space α] {β : Type u} [nonempty β] (p : α) (x : β) :

Every point is covered by chosen balls, before p.last_step.

theorem besicovitch.tau_package.color_lt {α : Type u_1} [metric_space α] {β : Type u} [nonempty β] (p : α) {i : ordinal} (hi : i < p.last_step) {N : } (hN : is_empty p.τ)) :
p.color i < N

If there are no configurations of satellites with N+1 points, one never uses more than N distinct families in the Besicovitch inductive construction.

theorem besicovitch.exist_disjoint_covering_families {α : Type u_1} [metric_space α] {β : Type u} {N : } {τ : } (hτ : 1 < τ) (hN : is_empty τ)) (q : α) :
∃ (s : fin Nset β), (∀ (i : fin N), (s i).pairwise_disjoint (λ (j : β), metric.closed_ball (q.c j) (q.r j))) ⋃ (i : fin N) (j : β) (H : j s i), metric.ball (q.c j) (q.r j)

The topological Besicovitch covering theorem: there exist finitely many families of disjoint balls covering all the centers in a package. More specifically, one can use N families if there are no satellite configurations with N+1 points.

### The measurable Besicovitch covering theorem #

theorem besicovitch.exist_finset_disjoint_balls_large_measure {α : Type u_1} [metric_space α] (μ : measure_theory.measure α) {N : } {τ : } (hτ : 1 < τ) (hN : is_empty τ)) (s : set α) (r : α → ) (rpos : ∀ (x : α), x s0 < r x) (rle : ∀ (x : α), x sr x 1) :
∃ (t : finset α), t s μ (s \ ⋃ (x : α) (H : x t), (r x)) (N / (N + 1)) * μ s t.pairwise_disjoint (λ (x : α), (r x))

Consider, for each x in a set s, a radius r x ∈ (0, 1]. Then one can find finitely many disjoint balls of the form closed_ball x (r x) covering a proportion 1/(N+1) of s, if there are no satellite configurations with N+1 points.

theorem besicovitch.exists_disjoint_closed_ball_covering_ae_of_finite_measure_aux {α : Type u_1} [metric_space α] [hb : has_besicovitch_covering α] (μ : measure_theory.measure α) (f : α → ) (s : set α) (hf : ∀ (x : α), x s(f x).nonempty) (hf' : ∀ (x : α), x sf x ) (hf'' : ∀ (x : α), x sInf (f x) 0) :
∃ (t : set × )), t.countable (∀ (p : α × ), p tp.fst s) (∀ (p : α × ), p tp.snd f p.fst) μ (s \ ⋃ (p : α × ) (hp : p t), p.snd) = 0 t.pairwise_disjoint (λ (p : α × ), p.snd)

The measurable Besicovitch covering theorem. Assume that, for any x in a set s, one is given a set of admissible closed balls centered at x, with arbitrarily small radii. Then there exists a disjoint covering of almost all s by admissible closed balls centered at some points of s. This version requires that the underlying measure is finite, and that the space has the Besicovitch covering property (which is satisfied for instance by normed real vector spaces). It expresses the conclusion in a slightly awkward form (with a subset of α × ℝ) coming from the proof technique. For a version assuming that the measure is sigma-finite, see exists_disjoint_closed_ball_covering_ae_aux. For a version giving the conclusion in a nicer form, see exists_disjoint_closed_ball_covering_ae.

theorem besicovitch.exists_disjoint_closed_ball_covering_ae_aux {α : Type u_1} [metric_space α] (μ : measure_theory.measure α) (f : α → ) (s : set α) (hf : ∀ (x : α), x s(f x).nonempty) (hf' : ∀ (x : α), x sf x ) (hf'' : ∀ (x : α), x sInf (f x) 0) :
∃ (t : set × )), t.countable (∀ (p : α × ), p tp.fst s) (∀ (p : α × ), p tp.snd f p.fst) μ (s \ ⋃ (p : α × ) (hp : p t), p.snd) = 0 t.pairwise_disjoint (λ (p : α × ), p.snd)

The measurable Besicovitch covering theorem. Assume that, for any x in a set s, one is given a set of admissible closed balls centered at x, with arbitrarily small radii. Then there exists a disjoint covering of almost all s by admissible closed balls centered at some points of s. This version requires that the underlying measure is sigma-finite, and that the space has the Besicovitch covering property (which is satisfied for instance by normed real vector spaces). It expresses the conclusion in a slightly awkward form (with a subset of α × ℝ) coming from the proof technique. For a version giving the conclusion in a nicer form, see exists_disjoint_closed_ball_covering_ae.

theorem besicovitch.exists_disjoint_closed_ball_covering_ae {α : Type u_1} [metric_space α] [hb : has_besicovitch_covering α] (μ : measure_theory.measure α) (f : α → ) (s : set α) (hf : ∀ (x : α), x s(f x).nonempty) (hf' : ∀ (x : α), x sf x ) (hf'' : ∀ (x : α), x sInf (f x) 0) :
∃ (t : set α) (r : α → ), t.countable t s (∀ (x : α), x tr x f x) μ (s \ ⋃ (x : α) (H : x t), (r x)) = 0 t.pairwise_disjoint (λ (x : α), (r x))

The measurable Besicovitch covering theorem. Assume that, for any x in a set s, one is given a set of admissible closed balls centered at x, with arbitrarily small radii. Then there exists a disjoint covering of almost all s by admissible closed balls centered at some points of s. This version requires that the underlying measure is sigma-finite, and that the space has the Besicovitch covering property (which is satisfied for instance by normed real vector spaces).

@[protected]
def besicovitch.vitali_family {α : Type u_1} [metric_space α] (μ : measure_theory.measure α)  :

In a space with the Besicovitch covering property, the set of closed balls with positive radius forms a Vitali family. This is essentially a restatement of the measurable Besicovitch theorem.

Equations