English
In a Besicovitch space, the collection of closed balls with positive radius forms a Vitali family for any finite measure μ.
Русский
В пространстве с свойством Бесиковитча множество замкнутых шаров с положительным радиусом образует Vitali-семейство для любой конечной меры μ.
LaTeX
$$$\text{Besicovitch.vitaliFamily}(\mu)\text{ is a Vitali family}$.$$
Lean4
/-- 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`. We can even require that the radius at `x`
is bounded by a given function `R x`. (Take `R = 1` if you don't need this additional feature).
This version requires the underlying measure to be sigma-finite, and the space to have the
Besicovitch covering property (which is satisfied for instance by normed real vector spaces).
-/
theorem exists_disjoint_closedBall_covering_ae (μ : Measure α) [SFinite μ] (f : α → Set ℝ) (s : Set α)
(hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty) (R : α → ℝ) (hR : ∀ x ∈ s, 0 < R x) :
∃ (t : Set α) (r : α → ℝ),
t.Countable ∧
t ⊆ s ∧
(∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧
μ (s \ ⋃ x ∈ t, closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun x => closedBall x (r x) :=
by
let g x := f x ∩ Ioo 0 (R x)
have hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty := fun x hx δ δpos ↦
by
rcases hf x hx (min δ (R x)) (lt_min δpos (hR x hx)) with ⟨r, hr⟩
exact ⟨r, ⟨⟨hr.1, hr.2.1, hr.2.2.trans_le (min_le_right _ _)⟩, ⟨hr.2.1, hr.2.2.trans_le (min_le_left _ _)⟩⟩⟩
rcases exists_disjoint_closedBall_covering_ae_aux μ g s hg with ⟨v, v_count, vs, vg, μv, v_disj⟩
obtain ⟨r, t, rfl⟩ : ∃ (r : α → ℝ) (t : Set α), v = graphOn r t :=
by
have I : ∀ p ∈ v, 0 ≤ p.2 := fun p hp => (vg p hp).2.1.le
rw [exists_eq_graphOn]
refine fun x hx y hy heq ↦ v_disj.eq hx hy <| not_disjoint_iff.2 ⟨x.1, ?_⟩
simp [*]
have hinj : InjOn (fun x ↦ (x, r x)) t := LeftInvOn.injOn (f₁' := Prod.fst) fun _ _ ↦ rfl
simp only [graphOn, forall_mem_image, biUnion_image, hinj.pairwiseDisjoint_image] at *
exact ⟨t, r, countable_of_injective_of_countable_image hinj v_count, vs, vg, μv, v_disj⟩
