# mathlib3documentation

measure_theory.covering.vitali

# Vitali covering theorems #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_closed_ball. 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 closed_ball x (3 * diam a) forms a Vitali family. This version is given in vitali.vitali_family.

theorem vitali.exists_disjoint_subfamily_covering_enlargment {α : Type u_1} {ι : Type u_2} (B : ι set α) (t : set ι) (δ : ι ) (τ : ) (hτ : 1 < τ) (δnonneg : (a : ι), a t 0 δ a) (R : ) (δle : (a : ι), a t δ a R) (hne : (a : ι), a t (B a).nonempty) :
(u : set ι) (H : u t), (a : ι), a t ( (b : ι) (H : b u), (B a B b).nonempty δ a τ * δ b)

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.

theorem vitali.exists_disjoint_subfamily_covering_enlargment_closed_ball {α : Type u_1} {ι : Type u_2} [metric_space α] (t : set ι) (x : ι α) (r : ι ) (R : ) (hr : (a : ι), a t r a R) :
(u : set ι) (H : u t), u.pairwise_disjoint (λ (a : ι), metric.closed_ball (x a) (r a)) (a : ι), a t ( (b : ι) (H : b u), metric.closed_ball (x a) (r a) metric.closed_ball (x b) (5 * r b))

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.

theorem vitali.exists_disjoint_covering_ae {α : Type u_1} {ι : Type u_2} [metric_space α] (μ : measure_theory.measure α) (s : set α) (t : set ι) (C : nnreal) (r : ι ) (c : ι α) (B : ι set α) (hB : (a : ι), a t B a metric.closed_ball (c a) (r a)) (μB : (a : ι), a t μ (metric.closed_ball (c a) (3 * r a)) C * μ (B a)) (ht : (a : ι), a t (interior (B a)).nonempty) (h't : (a : ι), a t is_closed (B a)) (hf : (x : α), x s (ε : ), ε > 0 ( (a : ι) (H : a t), r a ε c a = x)) :
(u : set ι) (H : u t), u.countable μ (s \ (a : ι) (H : a u), B a) = 0

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.

@[protected]
def vitali.vitali_family {α : Type u_1} [metric_space α] (μ : measure_theory.measure α) (C : nnreal) (h : (x : α), ∃ᶠ (r : ) in (set.Ioi 0), μ (3 * r)) C * μ r)) :

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 closed_ball x r and covering a fixed proportion 1/C of the ball closed_ball x (3 * r) forms a Vitali family. This is essentially a restatement of the measurable Vitali theorem.

Equations