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.

source

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), u.pairwise_disjoint B ∧ ∀ (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.

source

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.

source

theorem vitali.exists_disjoint_covering_ae {α : Type u_1} {ι : Type u_2} [metric_space α] [measurable_space α] [opens_measurable_space α] [topological_space.second_countable_topology α] (μ : measure_theory.measure α) [measure_theory.is_locally_finite_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 ∧ u.pairwise_disjoint B ∧ ⇑μ (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.

source

@[protected]

def vitali.vitali_family {α : Type u_1} [metric_space α] [measurable_space α] [opens_measurable_space α] [topological_space.second_countable_topology α] (μ : measure_theory.measure α) [measure_theory.is_locally_finite_measure μ] (C : nnreal) (h : ∀ (x : α), ∃ᶠ (r : ℝ) in nhds_within 0 (set.Ioi 0), ⇑μ (metric.closed_ball x (3 * r)) ≤ ↑C * ⇑μ (metric.closed_ball x r)) :

vitali_family μ

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

vitali.vitali_family μ C h = {sets_at := λ (x : α), {a : set α | is_closed a ∧ (interior a).nonempty ∧ ∃ (r : ℝ), a ⊆ metric.closed_ball x r ∧ ⇑μ (metric.closed_ball x (3 * r)) ≤ ↑C * ⇑μ a}, measurable_set' := _, nonempty_interior := _, nontrivial := _, covering := _}