mathlib documentation

measure_theory.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_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} (t : set (set α)) (δ : set α) (τ : ) (hτ : 1 < τ) (δnonneg : ∀ (a : set α), a t0 δ a) (R : ) (δle : ∀ (a : set α), a tδ a R) (hne : ∀ (a : set α), a t → a.nonempty) :
∃ (u : set (set α)) (H : u t), u.pairwise_disjoint id ∀ (a : set α), a t(∃ (b : set α) (H : b u), (a 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 / τ.

theorem vitali.exists_disjoint_subfamily_covering_enlargment_closed_ball {α : Type u_1} [metric_space α] (t : set (set α)) (R : ) (ht : ∀ (s : set α), s t(∃ (x : α) (r : ), s = metric.closed_ball x r r R)) :
∃ (u : set (set α)) (H : u t), u.pairwise_disjoint id ∀ (a : set α), a t(∃ (x : α) (r : ), metric.closed_ball x r u a metric.closed_ball x (5 * r))

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} [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 (set α)) (hf : ∀ (x : α), x s∀ (ε : ), ε > 0(∃ (a : set α) (H : a t), x a a metric.closed_ball x ε)) (ht : ∀ (a : set α), a t(interior a).nonempty) (h't : ∀ (a : set α), a tis_closed a) (C : ℝ≥0) (h : ∀ (a : set α), a t(∃ (x : α) (H : x a), μ (metric.closed_ball x (3 * metric.diam a)) (C) * μ a)) :
∃ (u : set (set α)) (H : u t), u.countable u.pairwise_disjoint id μ (s \ ⋃ (a : set α) (H : a u), 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, 6 r) for a given measure μ (think of the situation where μ is a doubling measure and t is a family of balls). Consider a (possible 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.

@[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 : ℝ≥0) (h : ∀ (x : α) (ε : ), ε > 0(∃ (r : ) (H : r set.Ioc 0 ε), μ (metric.closed_ball x (6 * r)) (C) * μ (metric.closed_ball x 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 covering a fixed proportion 1/C of the ball closed_ball x (3 * diam a) forms a Vitali family. This is essentially a restatement of the measurable Vitali theorem.

Equations