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.

theorem Vitali.exists_disjoint_subfamily_covering_enlargment {α : Type u_1} {ι : Type u_2} (B : ι → Set α) (t : Set ι) (δ : ι → ℝ) (τ : ℝ) (hτ : 1 < τ) (δnonneg : ∀ a ∈ t, 0 ≤ δ a) (R : ℝ) (δle : ∀ a ∈ t, δ a ≤ R) (hne : ∀ a ∈ t, Set.Nonempty (B a)) : ∃ u ⊆ t, Set.PairwiseDisjoint u B ∧ ∀ a ∈ t, ∃ b ∈ u, Set.Nonempty (B a ∩ B b) ∧ δ 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_closedBall {α : Type u_1} {ι : Type u_2} [MetricSpace α] (t : Set ι) (x : ι → α) (r : ι → ℝ) (R : ℝ) (hr : ∀ a ∈ t, r a ≤ R) : ∃ u ⊆ t, (Set.PairwiseDisjoint u fun (a : ι) => Metric.closedBall (x a) (r a)) ∧ ∀ a ∈ t, ∃ b ∈ u, Metric.closedBall (x a) (r a) ⊆ Metric.closedBall (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} [MetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set α) (t : Set ι) (C : NNReal) (r : ι → ℝ) (c : ι → α) (B : ι → Set α) (hB : ∀ a ∈ t, B a ⊆ Metric.closedBall (c a) (r a)) (μB : ∀ a ∈ t, ↑↑μ (Metric.closedBall (c a) (3 * r a)) ≤ ↑C * ↑↑μ (B a)) (ht : ∀ a ∈ t, Set.Nonempty (interior (B a))) (h't : ∀ a ∈ t, IsClosed (B a)) (hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x) : ∃ u ⊆ t, Set.Countable u ∧ Set.PairwiseDisjoint u B ∧ ↑↑μ (s \ ⋃ 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.

def Vitali.vitaliFamily {α : Type u_1} [MetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (C : NNReal) (h : ∀ (x : α), ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ↑↑μ (Metric.closedBall x (3 * r)) ≤ ↑C * ↑↑μ (Metric.closedBall x r)) : VitaliFamily μ

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.

Equations

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