Lean4
/-- 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. -/
theorem exist_disjoint_covering_families {N : ℕ} {τ : ℝ} (hτ : 1 < τ) (hN : IsEmpty (SatelliteConfig α N τ))
(q : BallPackage β α) :
∃ s : Fin N → Set β,
(∀ i : Fin N, (s i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)) ∧
range q.c ⊆ ⋃ i : Fin N, ⋃ j ∈ s i, ball (q.c j) (q.r j) :=
by
-- first exclude the trivial case where `β` is empty (we need non-emptiness for the transfinite
-- induction, to be able to choose garbage when there is no point left).
cases isEmpty_or_nonempty β
· refine ⟨fun _ => ∅, fun _ => pairwiseDisjoint_empty, ?_⟩
rw [← image_univ, eq_empty_of_isEmpty (univ : Set β)]
simp
-- Now, assume `β` is nonempty.
let p : TauPackage β α :=
{ q with
τ
one_lt_tau := hτ }
-- we use for `s i` the balls of color `i`.
let s := fun i : Fin N => ⋃ (k : Ordinal.{u}) (_ : k < p.lastStep) (_ : p.color k = i), ({p.index k} : Set β)
refine ⟨s, fun i => ?_, ?_⟩
· -- show that balls of the same color are disjoint
intro x hx y hy x_ne_y
obtain ⟨jx, jx_lt, jxi, rfl⟩ : ∃ jx : Ordinal, jx < p.lastStep ∧ p.color jx = i ∧ x = p.index jx := by
simpa only [s, exists_prop, mem_iUnion, mem_singleton_iff] using hx
obtain ⟨jy, jy_lt, jyi, rfl⟩ : ∃ jy : Ordinal, jy < p.lastStep ∧ p.color jy = i ∧ y = p.index jy := by
simpa only [s, exists_prop, mem_iUnion, mem_singleton_iff] using hy
wlog jxy : jx ≤ jy generalizing jx jy
· exact (this jy jy_lt jyi hy jx jx_lt jxi hx x_ne_y.symm (le_of_not_ge jxy)).symm
replace jxy : jx < jy := by rcases lt_or_eq_of_le jxy with (H | rfl);
· { exact H
};
· { exact (x_ne_y rfl).elim
}
let A : Set ℕ :=
⋃ (j : { j // j < jy }) (_ :
(closedBall (p.c (p.index j)) (p.r (p.index j)) ∩ closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
{p.color j}
have color_j : p.color jy = sInf (univ \ A) := by rw [TauPackage.color]
have h : p.color jy ∈ univ \ A := by
rw [color_j]
apply csInf_mem
refine ⟨N, ?_⟩
simp only [A, not_exists, true_and, exists_prop, mem_iUnion, mem_singleton_iff, not_and, mem_univ, mem_diff,
Subtype.exists]
intro k hk _
exact (p.color_lt (hk.trans jy_lt) hN).ne'
simp only [A, not_exists, true_and, exists_prop, mem_iUnion, mem_singleton_iff, not_and, mem_univ, mem_diff,
Subtype.exists] at h
specialize h jx jxy
contrapose! h
simpa only [jxi, jyi, and_true, eq_self_iff_true, ← not_disjoint_iff_nonempty_inter] using h
· -- show that the balls of color at most `N` cover every center.
refine range_subset_iff.2 fun b => ?_
obtain ⟨a, ha⟩ : ∃ a : Ordinal, a < p.lastStep ∧ dist (p.c b) (p.c (p.index a)) < p.r (p.index a) := by
simpa only [iUnionUpTo, exists_prop, mem_iUnion, mem_ball, Subtype.exists, Subtype.coe_mk] using
p.mem_iUnionUpTo_lastStep b
simp only [s, exists_prop, mem_iUnion, mem_ball, mem_singleton_iff, biUnion_and', exists_eq_left, iUnion_exists,
exists_and_left]
exact ⟨⟨p.color a, p.color_lt ha.1 hN⟩, a, rfl, ha⟩
