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`.
This version requires that the underlying measure is finite, and that the space has the Besicovitch
covering property (which is satisfied for instance by normed real vector spaces). It expresses the
conclusion in a slightly awkward form (with a subset of `α × ℝ`) coming from the proof technique.
For a version assuming that the measure is sigma-finite,
see `exists_disjoint_closedBall_covering_ae_aux`.
For a version giving the conclusion in a nicer form, see `exists_disjoint_closedBall_covering_ae`.
-/
theorem exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux (μ : Measure α) [IsFiniteMeasure μ] (f : α → Set ℝ)
(s : Set α) (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty) :
∃ t : Set (α × ℝ),
t.Countable ∧
(∀ p ∈ t, p.1 ∈ s) ∧
(∀ p ∈ t, p.2 ∈ f p.1) ∧
μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.1 p.2) = 0 ∧
t.PairwiseDisjoint fun p => closedBall p.1 p.2 :=
by
classical
rcases HasBesicovitchCovering.no_satelliteConfig (α := α) with
⟨N, τ, hτ, hN⟩
/- Introduce a property `P` on finsets saying that we have a nice disjoint covering of a
subset of `s` by admissible balls. -/
let P : Finset (α × ℝ) → Prop := fun t =>
((t : Set (α × ℝ)).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧
(∀ p : α × ℝ, p ∈ t → p.1 ∈ s) ∧
∀ p : α × ℝ,
p ∈ t →
p.2 ∈
f
p.1
/- Given a finite good covering of a subset `s`, one can find a larger finite good covering,
covering additionally a proportion at least `1/(N+1)` of leftover points. This follows from
`exist_finset_disjoint_balls_large_measure` applied to balls not intersecting the initial
covering. -/
have :
∀ t : Finset (α × ℝ),
P t →
∃ u : Finset (α × ℝ),
t ⊆ u ∧
P u ∧
μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ u), closedBall p.1 p.2) ≤
N / (N + 1) * μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.1 p.2) :=
by
intro t ht
set B := ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.1 p.2 with hB
have B_closed : IsClosed B := isClosed_biUnion_finset fun i _ => isClosed_closedBall
set s' := s \ B
have : ∀ x ∈ s', ∃ r ∈ f x ∩ Ioo 0 1, Disjoint B (closedBall x r) :=
by
intro x hx
have xs : x ∈ s := ((mem_diff x).1 hx).1
rcases eq_empty_or_nonempty B with (hB | hB)
· rcases hf x xs 1 zero_lt_one with ⟨r, hr, h'r⟩
exact ⟨r, ⟨hr, h'r⟩, by simp only [hB, empty_disjoint]⟩
· let r := infDist x B
have : 0 < min r 1 := lt_min ((B_closed.notMem_iff_infDist_pos hB).1 ((mem_diff x).1 hx).2) zero_lt_one
rcases hf x xs _ this with ⟨r, hr, h'r⟩
refine ⟨r, ⟨hr, ⟨h'r.1, h'r.2.trans_le (min_le_right _ _)⟩⟩, ?_⟩
rw [disjoint_comm]
exact disjoint_closedBall_of_lt_infDist (h'r.2.trans_le (min_le_left _ _))
choose! r hr using this
obtain ⟨v, vs', hμv, hv⟩ :
∃ v : Finset α,
↑v ⊆ s' ∧
μ (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤ N / (N + 1) * μ s' ∧
(v : Set α).PairwiseDisjoint fun x : α => closedBall x (r x) :=
haveI rI : ∀ x ∈ s', r x ∈ Ioo (0 : ℝ) 1 := fun x hx => (hr x hx).1.2
exist_finset_disjoint_balls_large_measure μ hτ hN s' r (fun x hx => (rI x hx).1) fun x hx => (rI x hx).2.le
refine ⟨t ∪ Finset.image (fun x => (x, r x)) v, Finset.subset_union_left, ⟨?_, ?_, ?_⟩, ?_⟩
· simp only [Finset.coe_union, pairwiseDisjoint_union, ht.1, true_and, Finset.coe_image]
constructor
· intro p hp q hq hpq
rcases (mem_image _ _ _).1 hp with ⟨p', p'v, rfl⟩
rcases (mem_image _ _ _).1 hq with ⟨q', q'v, rfl⟩
refine hv p'v q'v fun hp'q' => ?_
rw [hp'q'] at hpq
exact hpq rfl
· intro p hp q hq hpq
rcases (mem_image _ _ _).1 hq with ⟨q', q'v, rfl⟩
apply disjoint_of_subset_left _ (hr q' (vs' q'v)).2
rw [hB, ← Finset.set_biUnion_coe]
exact subset_biUnion_of_mem (u := fun x : α × ℝ => closedBall x.1 x.2) hp
· intro p hp
rcases Finset.mem_union.1 hp with (h'p | h'p)
· exact ht.2.1 p h'p
· rcases Finset.mem_image.1 h'p with ⟨p', p'v, rfl⟩
exact ((mem_diff _).1 (vs' (Finset.mem_coe.2 p'v))).1
· intro p hp
rcases Finset.mem_union.1 hp with (h'p | h'p)
· exact ht.2.2 p h'p
· rcases Finset.mem_image.1 h'p with ⟨p', p'v, rfl⟩
exact (hr p' (vs' p'v)).1.1
· convert hμv using 2
rw [Finset.set_biUnion_union, ← diff_diff, Finset.set_biUnion_finset_image]
/- Define `F` associating to a finite good covering the above enlarged good covering, covering
a proportion `1/(N+1)` of leftover points. Iterating `F`, one will get larger and larger good
coverings, missing in the end only a measure-zero set. -/
choose! F hF using this
let u n := F^[n] ∅
have u_succ : ∀ n : ℕ, u n.succ = F (u n) := fun n => by simp only [u, Function.comp_apply, Function.iterate_succ']
have Pu : ∀ n, P (u n) := by
intro n
induction n with
| zero =>
simp only [P, u, Prod.forall, id, Function.iterate_zero]
simp only [Finset.notMem_empty, IsEmpty.forall_iff, Finset.coe_empty, forall₂_true_iff, and_self_iff,
pairwiseDisjoint_empty]
| succ n IH =>
rw [u_succ]
exact (hF (u n) IH).2.1
refine ⟨⋃ n, u n, countable_iUnion fun n => (u n).countable_toSet, ?_, ?_, ?_, ?_⟩
· intro p hp
rcases mem_iUnion.1 hp with ⟨n, hn⟩
exact (Pu n).2.1 p (Finset.mem_coe.1 hn)
· intro p hp
rcases mem_iUnion.1 hp with ⟨n, hn⟩
exact (Pu n).2.2 p (Finset.mem_coe.1 hn)
· have A :
∀ n,
μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ ⋃ n : ℕ, (u n : Set (α × ℝ))), closedBall p.fst p.snd) ≤
μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ u n), closedBall p.fst p.snd) :=
by
intro n
gcongr μ (s \ ?_)
exact biUnion_subset_biUnion_left (subset_iUnion (fun i => (u i : Set (α × ℝ))) n)
have B : ∀ n, μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ u n), closedBall p.fst p.snd) ≤ (N / (N + 1) : ℝ≥0∞) ^ n * μ s :=
fun n ↦ by
induction n with
| zero =>
simp only [u, le_refl, diff_empty, one_mul, iUnion_false, iUnion_empty, pow_zero, Function.iterate_zero, id,
Finset.notMem_empty]
| succ n IH =>
calc
_ ≤ N / (N + 1) * μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ u n), closedBall p.fst p.snd) := by rw [u_succ];
exact (hF (u n) (Pu n)).2.2
_ ≤ _ := by rw [pow_succ', mul_assoc]; exact mul_le_mul_left' IH _
have C : Tendsto (fun n : ℕ => ((N : ℝ≥0∞) / (N + 1)) ^ n * μ s) atTop (𝓝 (0 * μ s)) :=
by
apply ENNReal.Tendsto.mul_const _ (Or.inr (measure_lt_top μ s).ne)
apply ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one
rw [ENNReal.div_lt_iff, one_mul]
· conv_lhs => rw [← add_zero (N : ℝ≥0∞)]
exact ENNReal.add_lt_add_left (ENNReal.natCast_ne_top N) zero_lt_one
· simp only [true_or, add_eq_zero, Ne, not_false_iff, one_ne_zero, and_false]
· left; finiteness
rw [zero_mul] at C
apply le_bot_iff.1
exact le_of_tendsto_of_tendsto' tendsto_const_nhds C fun n => (A n).trans (B n)
· refine (pairwiseDisjoint_iUnion ?_).2 fun n => (Pu n).1
apply (monotone_nat_of_le_succ fun n => ?_).directed_le
rw [← Nat.succ_eq_add_one, u_succ]
exact (hF (u n) (Pu n)).1
