Lean4
/-- **Vitali covering theorem**: given a set `t` of subsets of a type, one may extract a disjoint
subfamily `u` such that the `τ`-enlargement of this family covers all elements of `t`, where `τ > 1`
is any fixed number.
When `t` is a family of balls, the `τ`-enlargement of `ball x r` is `ball x ((1+2τ) r)`. In general,
it is expressed in terms of a function `δ` (think "radius" or "diameter"), positive and bounded on
all elements of `t`. The condition is that every element `a` of `t` should intersect an
element `b` of `u` of size larger than that of `a` up to `τ`, i.e., `δ b ≥ δ a / τ`.
We state the lemma slightly more generally, with an indexed family of sets `B a` for `a ∈ t`, for
wider applicability.
-/
theorem exists_disjoint_subfamily_covering_enlargement (B : ι → Set α) (t : Set ι) (δ : ι → ℝ) (τ : ℝ) (hτ : 1 < τ)
(δnonneg : ∀ a ∈ t, 0 ≤ δ a) (R : ℝ) (δle : ∀ a ∈ t, δ a ≤ R) (hne : ∀ a ∈ t, (B a).Nonempty) :
∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b := by
/- The proof could be formulated as a transfinite induction. First pick an element of `t` with `δ`
as large as possible (up to a factor of `τ`). Then among the remaining elements not intersecting
the already chosen one, pick another element with large `δ`. Go on forever (transfinitely) until
there is nothing left.
Instead, we give a direct Zorn-based argument. Consider a maximal family `u` of disjoint sets
with the following property: if an element `a` of `t` intersects some element `b` of `u`, then it
intersects some `b' ∈ u` with `δ b' ≥ δ a / τ`. Such a maximal family exists by Zorn. If this
family did not intersect some element `a ∈ t`, then take an element `a' ∈ t` which does not
intersect any element of `u`, with `δ a'` almost as large as possible. One checks easily
that `u ∪ {a'}` still has this property, contradicting the maximality. Therefore, `u`
intersects all elements of `t`, and by definition it satisfies all the desired properties.
-/
let T : Set (Set ι) :=
{u |
u ⊆ t ∧
u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
-- By Zorn, choose a maximal family in the good set `T` of disjoint families.
obtain ⟨u, hu⟩ : ∃ m, Maximal (fun x ↦ x ∈ T) m :=
by
refine zorn_subset _ fun U UT hU => ?_
refine ⟨⋃₀ U, ?_, fun s hs => subset_sUnion_of_mem hs⟩
simp only [T, Set.sUnion_subset_iff, and_imp, forall_exists_index, mem_sUnion, Set.mem_setOf_eq]
refine
⟨fun u hu => (UT hu).1, (pairwiseDisjoint_sUnion hU.directedOn).2 fun u hu => (UT hu).2.1,
fun a hat b u uU hbu hab => ?_⟩
obtain ⟨c, cu, ac, hc⟩ : ∃ c, c ∈ u ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c := (UT uU).2.2 a hat b hbu hab
exact
⟨c, ⟨u, uU, cu⟩, ac, hc⟩
-- The only nontrivial bit is to check that every `a ∈ t` intersects an element `b ∈ u` with
-- comparatively large `δ b`. Assume this is not the case, then we will contradict the maximality.
refine ⟨u, hu.prop.1, hu.prop.2.1, fun a hat => ?_⟩
by_contra! hcon
have a_disj : ∀ c ∈ u, Disjoint (B a) (B c) := by
intro c hc
by_contra h
rw [not_disjoint_iff_nonempty_inter] at h
obtain ⟨d, du, ad, hd⟩ : ∃ d, d ∈ u ∧ (B a ∩ B d).Nonempty ∧ δ a ≤ τ * δ d := hu.prop.2.2 a hat c hc h
exact
lt_irrefl _
((hcon d du ad).trans_le hd)
-- Let `A` be all the elements of `t` which do not intersect the family `u`. It is nonempty as it
-- contains `a`. We will pick an element `a'` of `A` with `δ a'` almost as large as possible.
let A := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
have Anonempty : A.Nonempty := ⟨a, hat, a_disj⟩
let m := sSup (δ '' A)
have bddA : BddAbove (δ '' A) := by
refine ⟨R, fun x xA => ?_⟩
rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩
exact δle a' ha'.1
obtain ⟨a', a'A, ha'⟩ : ∃ a' ∈ A, m / τ ≤ δ a' :=
by
have : 0 ≤ m := (δnonneg a hat).trans (le_csSup bddA (mem_image_of_mem _ ⟨hat, a_disj⟩))
rcases eq_or_lt_of_le this with (mzero | mpos)
· refine ⟨a, ⟨hat, a_disj⟩, ?_⟩
simpa only [← mzero, zero_div] using δnonneg a hat
· have I : m / τ < m := by
rw [div_lt_iff₀ (zero_lt_one.trans hτ)]
conv_lhs => rw [← mul_one m]
gcongr
rcases exists_lt_of_lt_csSup (Anonempty.image _) I with ⟨x, xA, hx⟩
rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩
exact ⟨a', ha', hx.le⟩
clear hat hcon a_disj a
have a'_ne_u : a' ∉ u := fun H =>
(hne _ a'A.1).ne_empty
(disjoint_self.1 (a'A.2 _ H))
-- we claim that `u ∪ {a'}` still belongs to `T`, contradicting the maximality of `u`.
refine a'_ne_u (hu.mem_of_prop_insert ⟨?_, ?_, ?_⟩)
· -- check that `u ∪ {a'}` is made of elements of `t`.
rw [insert_subset_iff]
exact ⟨a'A.1, hu.prop.1⟩
· -- Check that `u ∪ {a'}` is a disjoint family. This follows from the fact that `a'` does not
-- intersect `u`.
exact hu.prop.2.1.insert fun b bu _ => a'A.2 b bu
· -- check that every element `c` of `t` intersecting `u ∪ {a'}` intersects an element of this
-- family with large `δ`.
intro c ct b ba'u hcb
by_cases H : ∃ d ∈ u, (B c ∩ B d).Nonempty
· rcases H with ⟨d, du, hd⟩
rcases hu.prop.2.2 c ct d du hd with ⟨d', d'u, hd'⟩
exact ⟨d', mem_insert_of_mem _ d'u, hd'⟩
· -- Otherwise, `c` belongs to `A`. The element of `u ∪ {a'}` that it intersects has to be `a'`.
-- Moreover, `δ c` is smaller than the maximum `m` of `δ` over `A`, which is `≤ δ a' / τ`
-- thanks to the good choice of `a'`. This is the desired inequality.
push_neg at H
simp only [← disjoint_iff_inter_eq_empty] at H
rcases mem_insert_iff.1 ba'u with (rfl | H')
· refine ⟨b, mem_insert _ _, hcb, ?_⟩
calc
δ c ≤ m := le_csSup bddA (mem_image_of_mem _ ⟨ct, H⟩)
_ = τ * (m / τ) := by field_simp
_ ≤ τ * δ b := by gcongr
· rw [← not_disjoint_iff_nonempty_inter] at hcb
exact (hcb (H _ H')).elim
