Theorems · Theorem · measure theory

Vitali.exists_disjoint_covering_ae

• 1000+ list: Vitali covering theorem

∀ {α : Type u_1} {ι : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set α)
  (t : Set ι) (C : NNReal) (r : ι → ℝ) (c : ι → α) (B : ι → Set α),
  (∀ a ∈ t, B a ⊆ Metric.closedBall (c a) (r a)) →
    (∀ a ∈ t, μ (Metric.closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)) →
      (∀ a ∈ t, (interior (B a)).Nonempty) →
        (∀ a ∈ t, IsClosed (B a)) →
          (∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x) →
            ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint 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.

Defined in

Mathlib.MeasureTheory.Covering.Vitali

Cited by

1 results in Mathlib

Foundations

Depth 188 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceMeasurableSpaceOpensMeasurableSpaceSecondCountableTopologyMeasureTheory.IsLocallyFiniteMeasure