Lean4
/-- The measurable **Vitali covering theorem**.
Assume one is given a family `t` of closed sets with nonempty interior, such that each `a ∈ t` is
included in a ball `B (x, r)` and covers a definite proportion of the ball `B (x, 3 r)` for a given
measure `μ` (think of the situation where `μ` is a doubling measure and `t` is a family of balls).
Consider a (possibly non-measurable) set `s` at which the family is fine, i.e., every point of `s`
belongs to arbitrarily small elements of `t`. Then one can extract from `t` a disjoint subfamily
that covers almost all `s`.
For more flexibility, we give a statement with a parameterized family of sets.
-/
theorem exists_disjoint_covering_ae [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α]
[SecondCountableTopology α] (μ : Measure α) [IsLocallyFiniteMeasure μ] (s : Set α) (t : Set ι) (C : ℝ≥0) (r : ι → ℝ)
(c : ι → α) (B : ι → Set α) (hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a))
(μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ C * μ (B a)) (ht : ∀ a ∈ t, (interior (B a)).Nonempty)
(h't : ∀ a ∈ t, IsClosed (B a)) (hf : ∀ x ∈ s, ∀ ε > (0 : ℝ), ∃ a ∈ t, r a ≤ ε ∧ c a = x) :
∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0 := by
/- The idea of the proof is the following. Assume for simplicity that `μ` is finite. Applying the
abstract Vitali covering theorem with `δ = r` given by `hf`, one obtains a disjoint subfamily `u`,
such that any element of `t` intersects an element of `u` with comparable radius. Fix `ε > 0`.
Since the elements of `u` have summable measure, one can remove finitely elements `w_1, ..., w_n`.
so that the measure of the remaining elements is `< ε`. Consider now a point `z` not
in the `w_i`. There is a small ball around `z` not intersecting the `w_i` (as they are closed),
an element `a ∈ t` contained in this small ball (as the family `t` is fine at `z`) and an element
`b ∈ u` intersecting `a`, with comparable radius (by definition of `u`). Then `z` belongs to the
enlargement of `b`. This shows that `s \ (w_1 ∪ ... ∪ w_n)` is contained in
`⋃ (b ∈ u \ {w_1, ... w_n}) (enlargement of b)`. The measure of the latter set is bounded by
`∑ (b ∈ u \ {w_1, ... w_n}) C * μ b` (by the doubling property of the measure), which is at most
`C ε`. Letting `ε` tend to `0` shows that `s` is almost everywhere covered by the family `u`.
For the real argument, the measure is only locally finite. Therefore, we implement the same
strategy, but locally restricted to balls on which the measure is finite. For this, we do not
use the whole family `t`, but a subfamily `t'` supported on small balls (which is possible since
the family is assumed to be fine at every point of `s`).
-/
classical
-- choose around each `x` a small ball on which the measure is finite
have : ∀ x, ∃ R, 0 < R ∧ R ≤ 1 ∧ μ (closedBall x (20 * R)) < ∞ := fun x ↦
by
refine ((eventually_le_nhds one_pos).and ?_).exists_gt
refine (tendsto_closedBall_smallSets x).comp ?_ (μ.finiteAt_nhds x).eventually
exact Continuous.tendsto' (by fun_prop) _ _ (mul_zero _)
choose R hR0 hR1 hRμ using this
let t' :=
{a ∈ t | r a ≤ R (c a)}
-- extract a disjoint subfamily `u` of `t'` thanks to the abstract Vitali covering theorem.
obtain ⟨u, ut', u_disj, hu⟩ :
∃ u ⊆ t', u.PairwiseDisjoint B ∧ ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b :=
by
have A : ∀ a ∈ t', r a ≤ 1 := by
intro a ha
apply ha.2.trans (hR1 (c a))
have A' : ∀ a ∈ t', (B a).Nonempty := fun a hat' => Set.Nonempty.mono interior_subset (ht a hat'.1)
refine exists_disjoint_subfamily_covering_enlargement B t' r 2 one_lt_two (fun a ha => ?_) 1 A A'
exact nonempty_closedBall.1 ((A' a ha).mono (hB a ha.1))
have ut : u ⊆ t := fun a hau =>
(ut' hau).1
-- As the space is second countable, the family is countable since all its sets have nonempty
-- interior.
have u_count : u.Countable :=
u_disj.countable_of_nonempty_interior fun a ha =>
ht a
(ut ha)
-- the family `u` will be the desired family
refine
⟨u, fun a hat' => (ut' hat').1, u_count, u_disj, ?_⟩
-- it suffices to show that it covers almost all `s` locally around each point `x`.
refine
measure_null_of_locally_null _ fun x _ =>
?_
-- let `v` be the subfamily of `u` made of those sets intersecting the small ball `ball x (r x)`
let v := {a ∈ u | (B a ∩ ball x (R x)).Nonempty}
have vu : v ⊆ u := fun a ha =>
ha.1
-- they are all contained in a fixed ball of finite measure, thanks to our choice of `t'`
obtain ⟨K, μK, hK⟩ : ∃ K, μ (closedBall x K) < ∞ ∧ ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K :=
by
have Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x := by
intro a hav
apply dist_le_add_of_nonempty_closedBall_inter_closedBall
refine hav.2.mono ?_
apply inter_subset_inter _ ball_subset_closedBall
exact hB a (ut (vu hav))
set R0 := sSup (r '' v) with R0_def
have R0_bdd : BddAbove (r '' v) := by
refine ⟨1, fun r' hr' => ?_⟩
rcases (mem_image _ _ _).1 hr' with ⟨b, hb, rfl⟩
exact le_trans (ut' (vu hb)).2 (hR1 (c b))
rcases le_total R0 (R x) with (H | H)
· refine ⟨20 * R x, hRμ x, fun a au hax => ?_⟩
refine (hB a (ut au)).trans ?_
apply closedBall_subset_closedBall'
have : r a ≤ R0 := le_csSup R0_bdd (mem_image_of_mem _ ⟨au, hax⟩)
linarith [Idist_v a ⟨au, hax⟩, hR0 x]
· have R0pos : 0 < R0 := (hR0 x).trans_le H
have vnonempty : v.Nonempty := by
by_contra h
rw [nonempty_iff_ne_empty, Classical.not_not] at h
rw [h, image_empty, Real.sSup_empty] at R0_def
exact lt_irrefl _ (R0pos.trans_le (le_of_eq R0_def))
obtain ⟨a, hav, R0a⟩ : ∃ a ∈ v, R0 / 2 < r a :=
by
obtain ⟨r', r'mem, hr'⟩ : ∃ r' ∈ r '' v, R0 / 2 < r' :=
exists_lt_of_lt_csSup (vnonempty.image _) (half_lt_self R0pos)
rcases (mem_image _ _ _).1 r'mem with ⟨a, hav, rfl⟩
exact ⟨a, hav, hr'⟩
refine ⟨8 * R0, ?_, ?_⟩
· apply lt_of_le_of_lt (measure_mono _) (hRμ (c a))
apply closedBall_subset_closedBall'
rw [dist_comm]
linarith [Idist_v a hav, (ut' (vu hav)).2]
· intro b bu hbx
refine (hB b (ut bu)).trans ?_
apply closedBall_subset_closedBall'
have : r b ≤ R0 := le_csSup R0_bdd (mem_image_of_mem _ ⟨bu, hbx⟩)
linarith [Idist_v b ⟨bu, hbx⟩]
-- we will show that, in `ball x (R x)`, almost all `s` is covered by the family `u`.
refine
⟨_ ∩ ball x (R x), inter_mem_nhdsWithin _ (ball_mem_nhds _ (hR0 _)),
nonpos_iff_eq_zero.mp (le_of_forall_gt_imp_ge_of_dense fun ε εpos => ?_)⟩
-- the elements of `v` are disjoint and all contained in a finite volume ball, hence the sum
-- of their measures is finite.
have I : (∑' a : v, μ (B a)) < ∞ := by
calc
(∑' a : v, μ (B a)) = μ (⋃ a ∈ v, B a) :=
by
rw [measure_biUnion (u_count.mono vu) _ fun a ha => (h't _ (vu.trans ut ha)).measurableSet]
exact u_disj.subset vu
_ ≤ μ (closedBall x K) := (measure_mono (iUnion₂_subset fun a ha => hK a (vu ha) ha.2))
_ < ∞ := μK
obtain ⟨w, hw⟩ : ∃ w : Finset v, (∑' a : { a // a ∉ w }, μ (B a)) < ε / C :=
haveI : 0 < ε / C := by
simp only [ENNReal.div_pos_iff, εpos.ne', ENNReal.coe_ne_top, Ne, not_false_iff, and_self_iff]
((tendsto_order.1 (ENNReal.tendsto_tsum_compl_atTop_zero I.ne)).2 _ this).exists
have M : (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆ ⋃ a : { a // a ∉ w }, closedBall (c a) (3 * r a) :=
by
intro z hz
set k := ⋃ (a : v) (_ : a ∈ w), B a
have k_closed : IsClosed k := isClosed_biUnion_finset fun i _ => h't _ (ut (vu i.2))
have z_notmem_k : z ∉ k :=
by
simp only [k, not_exists, exists_prop, mem_iUnion, forall_exists_index, SetCoe.exists, not_and, exists_and_right]
intro b hbv _ h'z
have : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ⋃ a ∈ u, B a := mem_inter (mem_of_mem_inter_left hz) (mem_biUnion (vu hbv) h'z)
simpa only [diff_inter_self]
-- since the elements of `w` are closed and finitely many, one can find a small ball around `z`
-- not intersecting them
have : ball x (R x) \ k ∈ 𝓝 z :=
by
apply IsOpen.mem_nhds (isOpen_ball.sdiff k_closed) _
exact (mem_diff _).2 ⟨mem_of_mem_inter_right hz, z_notmem_k⟩
obtain ⟨d, dpos, hd⟩ : ∃ d, 0 < d ∧ closedBall z d ⊆ ball x (R x) \ k := nhds_basis_closedBall.mem_iff.1 this
obtain ⟨a, hat, ad, rfl⟩ : ∃ a ∈ t, r a ≤ min d (R z) ∧ c a = z :=
hf z ((mem_diff _).1 (mem_of_mem_inter_left hz)).1 (min d (R z)) (lt_min dpos (hR0 z))
have ax : B a ⊆ ball x (R x) := by
refine (hB a hat).trans ?_
refine Subset.trans ?_ (hd.trans Set.diff_subset)
exact
closedBall_subset_closedBall
(ad.trans (min_le_left _ _))
-- it intersects an element `b` of `u` with comparable diameter, by definition of `u`
obtain ⟨b, bu, ab, bdiam⟩ : ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b := hu a ⟨hat, ad.trans (min_le_right _ _)⟩
have bv : b ∈ v := by
refine ⟨bu, ab.mono ?_⟩
rw [inter_comm]
exact inter_subset_inter_right _ ax
let b' : v :=
⟨b, bv⟩
-- `b` cannot belong to `w`, as the elements of `w` do not intersect `closedBall z d`,
-- contrary to `b`
have b'_notmem_w : b' ∉ w := by
intro b'w
have b'k : B b' ⊆ k := @Finset.subset_set_biUnion_of_mem _ _ _ (fun y : v => B y) _ b'w
have : (ball x (R x) \ k ∩ k).Nonempty :=
by
apply ab.mono (inter_subset_inter _ b'k)
refine ((hB _ hat).trans ?_).trans hd
exact closedBall_subset_closedBall (ad.trans (min_le_left _ _))
simpa only [diff_inter_self, Set.not_nonempty_empty]
let b'' : { a // a ∉ w } :=
⟨b', b'_notmem_w⟩
-- since `a` and `b` have comparable diameters, it follows that `z` belongs to the
-- enlargement of `b`
have zb : c a ∈ closedBall (c b) (3 * r b) :=
by
rcases ab with ⟨e, ⟨ea, eb⟩⟩
have A : dist (c a) e ≤ r a := mem_closedBall'.1 (hB a hat ea)
have B : dist e (c b) ≤ r b := mem_closedBall.1 (hB b (ut bu) eb)
simp only [mem_closedBall]
linarith only [dist_triangle (c a) e (c b), A, B, bdiam]
suffices H : closedBall (c b'') (3 * r b'') ⊆ ⋃ a : { a // a ∉ w }, closedBall (c a) (3 * r a) from H zb
exact subset_iUnion (fun a : { a // a ∉ w } => closedBall (c a) (3 * r a)) b''
haveI : Countable v := (u_count.mono vu).to_subtype
calc
μ ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ μ (⋃ a : { a // a ∉ w }, closedBall (c a) (3 * r a)) := measure_mono M
_ ≤ ∑' a : { a // a ∉ w }, μ (closedBall (c a) (3 * r a)) := (measure_iUnion_le _)
_ ≤ ∑' a : { a // a ∉ w }, C * μ (B a) := (ENNReal.tsum_le_tsum fun a => μB a (ut (vu a.1.2)))
_ = C * ∑' a : { a // a ∉ w }, μ (B a) := ENNReal.tsum_mul_left
_ ≤ C * (ε / C) := by gcongr
_ ≤ ε := ENNReal.mul_div_le
