# 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_closedBall_covering_ae`

.

This implies that balls of small radius form a Vitali family in such spaces. Therefore, theorems on differentiation of measures hold as a consequence of general results. We restate them in this context to make them more easily usable.

## Main definitions and results #

`SatelliteConfig α N τ`

is the type of all satellite configurations of`N + 1`

points in the metric space`α`

, with parameter`τ`

.`HasBesicovitchCovering`

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_closedBall_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`HasBesicovitchCovering`

.

We also restate the following specialized versions of general theorems on differentiation of measures:

`Besicovitch.ae_tendsto_rnDeriv`

ensures that`ρ (closedBall x r) / μ (closedBall x r)`

tends almost surely to the Radon-Nikodym derivative of`ρ`

with respect to`μ`

at`x`

.`Besicovitch.ae_tendsto_measure_inter_div`

states that almost every point in an arbitrary set`s`

is a Lebesgue density point, i.e.,`μ (s ∩ closedBall x r) / μ (closedBall x r)`

tends to`1`

as`r`

tends to`0`

. A stronger version for measurable sets is given in`Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet`

.

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

- rpos : ∀ (i : Fin (Nat.succ N)), 0 < Besicovitch.SatelliteConfig.r s i
- h : ∀ (i j : Fin (Nat.succ N)), i ≠ j → Besicovitch.SatelliteConfig.r s i ≤ dist (Besicovitch.SatelliteConfig.c s i) (Besicovitch.SatelliteConfig.c s j) ∧ Besicovitch.SatelliteConfig.r s j ≤ τ * Besicovitch.SatelliteConfig.r s i ∨ Besicovitch.SatelliteConfig.r s j ≤ dist (Besicovitch.SatelliteConfig.c s j) (Besicovitch.SatelliteConfig.c s i) ∧ Besicovitch.SatelliteConfig.r s i ≤ τ * Besicovitch.SatelliteConfig.r s j
- hlast : ∀ (i : Fin (N + 1)), i < Fin.last N → Besicovitch.SatelliteConfig.r s i ≤ dist (Besicovitch.SatelliteConfig.c s i) (Besicovitch.SatelliteConfig.c s (Fin.last N)) ∧ Besicovitch.SatelliteConfig.r s (Fin.last N) ≤ τ * Besicovitch.SatelliteConfig.r s i
- inter : ∀ (i : Fin (N + 1)), i < Fin.last N → dist (Besicovitch.SatelliteConfig.c s i) (Besicovitch.SatelliteConfig.c s (Fin.last N)) ≤ Besicovitch.SatelliteConfig.r s i + Besicovitch.SatelliteConfig.r s (Fin.last N)

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`

.

## Instances For

- no_satelliteConfig : ∃ N τ, 1 < τ ∧ IsEmpty (Besicovitch.SatelliteConfig α N τ)

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 satisfied by
finite-dimensional real vector spaces.

## Instances

There is always a satellite configuration with a single point.

### Extracting disjoint subfamilies from a ball covering #

- c : β → α
- r : β → ℝ
- rpos : ∀ (b : β), 0 < Besicovitch.BallPackage.r s b
- r_bound : ℝ
- r_le : ∀ (b : β), Besicovitch.BallPackage.r s b ≤ s.r_bound

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

## Instances For

The ball package made of unit balls.

## Instances For

- c : β → α
- r : β → ℝ
- rpos : ∀ (b : β), 0 < Besicovitch.BallPackage.r s.toBallPackage b
- r_bound : ℝ
- r_le : ∀ (b : β), Besicovitch.BallPackage.r s.toBallPackage b ≤ s.r_bound
- τ : ℝ
- one_lt_tau : 1 < s.τ

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.

## Instances For

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

## Equations

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

## Instances For

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

.

## Instances For

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

.

## Instances For

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

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

## Instances For

`p.lastStep`

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.

## Instances For

Every point is covered by chosen balls, before `p.lastStep`

.

If there are no configurations of satellites with `N+1`

points, one never uses more than `N`

distinct families in the Besicovitch inductive construction.

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 #

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 `closedBall x (r x)`

covering a proportion `1/(N+1)`

of `s`

, if
there are no satellite configurations with `N+1`

points.

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_closedBall_covering_ae_aux`

.
For a version giving the conclusion in a nicer form, see `exists_disjoint_closedBall_covering_ae`

.

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_closedBall_covering_ae`

.

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`

. We can even require that the radius at `x`

is bounded by a given function `R x`

.
(Take `R = 1`

if you don't need this additional feature).
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).

In a space with the Besicovitch property, any set `s`

can be covered with balls whose measures
add up to at most `μ s + ε`

, for any positive `ε`

. This works even if one restricts the set of
allowed radii around a point `x`

to a set `f x`

which accumulates at `0`

.

### Consequences on differentiation of measures #

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.

## Instances For

The main feature of the Besicovitch Vitali family is that its filter at a point `x`

corresponds
to convergence along closed balls. We record one of the two implications here, which will enable us
to deduce specific statements on differentiation of measures in this context from the general
versions.

In a space with the Besicovitch covering property, the ratio of the measure of balls converges almost surely to the Radon-Nikodym derivative.

Given a measurable set `s`

, then `μ (s ∩ closedBall x r) / μ (closedBall x r)`

converges when
`r`

tends to `0`

, for almost every `x`

. The limit is `1`

for `x ∈ s`

and `0`

for `x ∉ s`

.
This shows that almost every point of `s`

is a Lebesgue density point for `s`

.
A version for non-measurable sets holds, but it only gives the first conclusion,
see `ae_tendsto_measure_inter_div`

.

Given an arbitrary set `s`

, then `μ (s ∩ closedBall x r) / μ (closedBall x r)`

converges
to `1`

when `r`

tends to `0`

, for almost every `x`

in `s`

.
This shows that almost every point of `s`

is a Lebesgue density point for `s`

.
A stronger version holds for measurable sets, see `ae_tendsto_measure_inter_div_of_measurableSet`

.

See also `IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div`

.