# Vitali covering theorems #

The topological Vitali covering theorem, in its most classical version, states the following.
Consider a family of balls `(B (x_i, r_i))_{i ∈ I}`

in a metric space, with uniformly bounded
radii. Then one can extract a disjoint subfamily indexed by `J ⊆ I`

, such that any `B (x_i, r_i)`

is included in a ball `B (x_j, 5 r_j)`

.

We prove this theorem in `Vitali.exists_disjoint_subfamily_covering_enlargment_closedBall`

.
It is deduced from a more general version, called
`Vitali.exists_disjoint_subfamily_covering_enlargment`

, which applies to any family of sets
together with a size function `δ`

(think "radius" or "diameter").

We deduce the measurable Vitali covering theorem. Assume one is given a family `t`

of closed sets
with nonempty interior, such that each `a ∈ t`

is included in a ball `B (x, r)`

and covers a
definite proportion of the ball `B (x, 6 r)`

for a given measure `μ`

(think of the situation
where `μ`

is a doubling measure and `t`

is a family of balls). Consider a set `s`

at which the
family is fine, i.e., every point of `s`

belongs to arbitrarily small elements of `t`

. Then one
can extract from `t`

a disjoint subfamily that covers almost all `s`

. It is proved in
`Vitali.exists_disjoint_covering_ae`

.

A way to restate this theorem is to say that the set of closed sets `a`

with nonempty interior
covering a fixed proportion `1/C`

of the ball `closedBall x (3 * diam a)`

forms a Vitali family.
This version is given in `Vitali.vitaliFamily`

.

Vitali covering theorem: given a set `t`

of subsets of a type, one may extract a disjoint
subfamily `u`

such that the `τ`

-enlargment of this family covers all elements of `t`

, where `τ > 1`

is any fixed number.

When `t`

is a family of balls, the `τ`

-enlargment of `ball x r`

is `ball x ((1+2τ) r)`

. In general,
it is expressed in terms of a function `δ`

(think "radius" or "diameter"), positive and bounded on
all elements of `t`

. The condition is that every element `a`

of `t`

should intersect an
element `b`

of `u`

of size larger than that of `a`

up to `τ`

, i.e., `δ b ≥ δ a / τ`

.

We state the lemma slightly more generally, with an indexed family of sets `B a`

for `a ∈ t`

, for
wider applicability.

Vitali covering theorem, closed balls version: given a family `t`

of closed balls, one can
extract a disjoint subfamily `u ⊆ t`

so that all balls in `t`

are covered by the 5-times
dilations of balls in `u`

.

The measurable Vitali covering theorem. Assume one is given a family `t`

of closed sets with
nonempty interior, such that each `a ∈ t`

is included in a ball `B (x, r)`

and covers a definite
proportion of the ball `B (x, 3 r)`

for a given measure `μ`

(think of the situation where `μ`

is
a doubling measure and `t`

is a family of balls). Consider a (possibly non-measurable) set `s`

at which the family is fine, i.e., every point of `s`

belongs to arbitrarily small elements of `t`

.
Then one can extract from `t`

a disjoint subfamily that covers almost all `s`

.

For more flexibility, we give a statement with a parameterized family of sets.

Assume that around every point there are arbitrarily small scales at which the measure is
doubling. Then the set of closed sets `a`

with nonempty interior contained in `closedBall x r`

and
covering a fixed proportion `1/C`

of the ball `closedBall x (3 * r)`

forms a Vitali family.
This is essentially a restatement of the measurable Vitali theorem.