Theorems · Theorem · measure theory

Besicovitch.exists_disjoint_closedBall_covering_ae_aux

∀ {α : Type u_1} [inst : MetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α]
  [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ]
  (f : α → Set ℝ) (s : Set α),
  (∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) →
    ∃ t,
      t.Countable ∧
        (∀ p ∈ t, p.1 ∈ s) ∧
          (∀ p ∈ t, p.2 ∈ f p.1) ∧
            μ (s \ ⋃ p ∈ t, Metric.closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => Metric.closedBall p.1 p.2

The measurable Besicovitch covering theorem. Assume that, for any x in a set s, one is given a set of admissible closed balls centered at x, with arbitrarily small radii. Then there exists a disjoint covering of almost all s by admissible closed balls centered at some points of s. This version requires the underlying measure to be s-finite, and the space to have the Besicovitch covering property (which is satisfied for instance by finite-dimensional normed real vector spaces). It expresses the conclusion in a slightly awkward form (with a subset of α × ℝ) coming from the proof technique. For a version giving the conclusion in a nicer form, see exists_disjoint_closedBall_covering_ae.

Defined in

Mathlib.MeasureTheory.Covering.Besicovitch

Cited by

1 results in Mathlib

Foundations

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

Assumes

MetricSpaceSecondCountableTopologyMeasurableSpaceOpensMeasurableSpaceHasBesicovitchCoveringMeasureTheory.SFinite