Theorems · Theorem · measure theory

Besicovitch.exist_disjoint_covering_families

∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} {N : ℕ} {τ : ℝ},
  1 < τ →
    IsEmpty (Besicovitch.SatelliteConfig α N τ) →
      ∀ (q : Besicovitch.BallPackage β α),
        ∃ s,
          (∀ (i : Fin N), (s i).PairwiseDisjoint fun j => Metric.closedBall (q.c j) (q.r j)) ∧
            Set.range q.c ⊆ ⋃ i, ⋃ j ∈ s i, Metric.ball (q.c j) (q.r j)

The topological Besicovitch covering theorem: there exist finitely many families of disjoint balls covering all the centers in a package. More specifically, one can use N families if there are no satellite configurations with N+1 points.

Defined in

Mathlib.MeasureTheory.Covering.Besicovitch

Cited by

2 results in Mathlib

Foundations

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

Assumes

MetricSpace