English
A Vitali-type theorem for closed balls: one can extract a disjoint subfamily of closed balls whose τ-enlargements cover the original collection.
Русский
Теорема Витали для закрытых шаров: можно извлечь непересекающуюся подподборку закрытых шаров, чье τ-расширение покрывает исходную коллекцию.
LaTeX
$$$\exists u\subseteq t,\ (u.plain)\ PairwiseDisjoint (\lambda a.\overline{B(x_a,r_a)}) ∧ \forall a∈t, ∃ b∈u,\overline{B(x_a,r_a)} ⊆ \overline{B(x_b, τ r_b)}.$$$
Lean4
/-- Vitali covering theorem, closed balls version: given a family `t` of closed balls, one can
extract a disjoint subfamily `u ⊆ t` so that all balls in `t` are covered by the τ-times
dilations of balls in `u`, for some `τ > 3`. -/
theorem exists_disjoint_subfamily_covering_enlargement_closedBall [PseudoMetricSpace α] (t : Set ι) (x : ι → α)
(r : ι → ℝ) (R : ℝ) (hr : ∀ a ∈ t, r a ≤ R) (τ : ℝ) (hτ : 3 < τ) :
∃ u ⊆ t,
(u.PairwiseDisjoint fun a => closedBall (x a) (r a)) ∧
∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b) :=
by
rcases eq_empty_or_nonempty t with (rfl | _)
· exact ⟨∅, Subset.refl _, pairwiseDisjoint_empty, by simp⟩
by_cases ht : ∀ a ∈ t, r a < 0
·
exact
⟨t, Subset.rfl, fun a ha b _ _ => by simp only [closedBall_eq_empty.2 (ht a ha), empty_disjoint, Function.onFun],
fun a ha => ⟨a, ha, by simp only [closedBall_eq_empty.2 (ht a ha), empty_subset]⟩⟩
push_neg at ht
let t' := {a ∈ t | 0 ≤ r a}
rcases
exists_disjoint_subfamily_covering_enlargement (fun a => closedBall (x a) (r a)) t' r ((τ - 1) / 2) (by linarith)
(fun a ha => ha.2) R (fun a ha => hr a ha.1) fun a ha => ⟨x a, mem_closedBall_self ha.2⟩ with
⟨u, ut', u_disj, hu⟩
have A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b) :=
by
intro a ha
rcases hu a ha with ⟨b, bu, hb, rb⟩
refine ⟨b, bu, ?_⟩
have : dist (x a) (x b) ≤ r a + r b := dist_le_add_of_nonempty_closedBall_inter_closedBall hb
apply closedBall_subset_closedBall'
linarith
refine ⟨u, ut'.trans fun a ha => ha.1, u_disj, fun a ha => ?_⟩
rcases le_or_gt 0 (r a) with (h'a | h'a)
· exact A a ⟨ha, h'a⟩
· rcases ht with ⟨b, rb⟩
rcases A b ⟨rb.1, rb.2⟩ with ⟨c, cu, _⟩
exact ⟨c, cu, by simp only [closedBall_eq_empty.2 h'a, empty_subset]⟩
