Documentation

Mathlib.MeasureTheory.Covering.Vitali

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 : at, 0 δ a) (R : ) (δle : at, δ a R) (hne : at, (B a).Nonempty) :
ut, u.PairwiseDisjoint B at, bu, (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_closedBall {α : Type u_1} {ι : Type u_2} [MetricSpace α] (t : Set ι) (x : ια) (r : ι) (R : ) (hr : at, r a R) (τ : ) (hτ : 3 < τ) :
ut, (u.PairwiseDisjoint fun (a : ι) => Metric.closedBall (x a) (r a)) at, bu, Metric.closedBall (x a) (r a) Metric.closedBall (x b) (τ * 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 τ-times dilations of balls in u, for some τ > 3.

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 : at, B a Metric.closedBall (c a) (r a)) (μB : at, μ (Metric.closedBall (c a) (3 * r a)) C * μ (B a)) (ht : at, (interior (B a)).Nonempty) (h't : at, IsClosed (B a)) (hf : xs, ε > 0, at, r a ε c a = x) :
ut, u.Countable u.PairwiseDisjoint B μ (s \ au, 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.

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.
Instances For