Theorems · Theorem · measure theory

Besicovitch.exists_closedBall_covering_tsum_measure_le

∀ {α : Type u_1} [inst : MetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α]
  [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ]
  [μ.OuterRegular] {ε : ENNReal},
  ε ≠ 0 →
    ∀ (f : α → Set ℝ) (s : Set α),
      (∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) →
        ∃ t r,
          t.Countable ∧
            t ⊆ s ∧
              (∀ x ∈ t, r x ∈ f x) ∧
                s ⊆ ⋃ x ∈ t, Metric.closedBall x (r x) ∧ ∑' (x : ↑t), μ (Metric.closedBall (↑x) (r ↑x)) ≤ μ s + ε

In a space with the Besicovitch property, any set s can be covered with balls whose measures add up to at most μ s + ε, for any positive ε. This works even if one restricts the set of allowed radii around a point x to a set f x which accumulates at 0.

Defined in

Mathlib.MeasureTheory.Covering.Besicovitch

Cited by

1 results in Mathlib

Foundations

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

Assumes

MetricSpaceSecondCountableTopologyMeasurableSpaceOpensMeasurableSpaceHasBesicovitchCoveringMeasureTheory.SFiniteMeasureTheory.Measure.OuterRegular