Lean4
/-- Consider, for each `x` in a set `s`, a radius `r x ∈ (0, 1]`. Then one can find finitely
many disjoint balls of the form `closedBall x (r x)` covering a proportion `1/(N+1)` of `s`, if
there are no satellite configurations with `N+1` points.
-/
theorem exist_finset_disjoint_balls_large_measure (μ : Measure α) [IsFiniteMeasure μ] {N : ℕ} {τ : ℝ} (hτ : 1 < τ)
(hN : IsEmpty (SatelliteConfig α N τ)) (s : Set α) (r : α → ℝ) (rpos : ∀ x ∈ s, 0 < r x) (rle : ∀ x ∈ s, r x ≤ 1) :
∃ t : Finset α,
↑t ⊆ s ∧
μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ N / (N + 1) * μ s ∧
(t : Set α).PairwiseDisjoint fun x => closedBall x (r x) :=
by
classical
-- exclude the trivial case where `μ s = 0`.
rcases le_or_gt (μ s) 0 with (hμs | hμs)
· have : μ s = 0 := le_bot_iff.1 hμs
refine ⟨∅, by simp only [Finset.coe_empty, empty_subset], ?_, ?_⟩
· simp only [this, Finset.notMem_empty, diff_empty, iUnion_false, iUnion_empty, nonpos_iff_eq_zero, mul_zero]
· simp only [Finset.coe_empty, pairwiseDisjoint_empty]
cases isEmpty_or_nonempty α
· simp only [eq_empty_of_isEmpty s, measure_empty] at hμs
exact (lt_irrefl _ hμs).elim
have Npos : N ≠ 0 := by
rintro rfl
inhabit α
exact not_isEmpty_of_nonempty _ hN
obtain ⟨o, so, omeas, μo⟩ : ∃ o : Set α, s ⊆ o ∧ MeasurableSet o ∧ μ o = μ s := exists_measurable_superset μ s
let a : BallPackage s α :=
{ c := fun x => x
r := fun x => r x
rpos := fun x => rpos x x.2
r_bound := 1
r_le := fun x => rle x x.2 }
rcases exist_disjoint_covering_families hτ hN a with ⟨u, hu, hu'⟩
have u_count : ∀ i, (u i).Countable := by
intro i
refine (hu i).countable_of_nonempty_interior fun j _ => ?_
have : (ball (j : α) (r j)).Nonempty := nonempty_ball.2 (a.rpos _)
exact this.mono ball_subset_interior_closedBall
let v : Fin N → Set α := fun i => ⋃ (x : s) (_ : x ∈ u i), closedBall x (r x)
have A : s = ⋃ i : Fin N, s ∩ v i :=
by
refine Subset.antisymm ?_ (iUnion_subset fun i => inter_subset_left)
intro x hx
obtain ⟨i, y, hxy, h'⟩ : ∃ (i : Fin N) (i_1 : ↥s), i_1 ∈ u i ∧ x ∈ ball (↑i_1) (r ↑i_1) :=
by
have : x ∈ range a.c := by simpa only [a, Subtype.range_coe_subtype, setOf_mem_eq]
simpa only [mem_iUnion, bex_def] using hu' this
refine mem_iUnion.2 ⟨i, ⟨hx, ?_⟩⟩
simp only [v, exists_prop, mem_iUnion, SetCoe.exists, exists_and_right]
exact ⟨y, ⟨y.2, by simpa only [Subtype.coe_eta]⟩, ball_subset_closedBall h'⟩
have S : ∑ _i : Fin N, μ s / N ≤ ∑ i, μ (s ∩ v i) :=
calc
∑ _i : Fin N, μ s / N = μ s :=
by
simp only [Finset.card_fin, Finset.sum_const, nsmul_eq_mul]
rw [ENNReal.mul_div_cancel]
· simp only [Npos, Ne, Nat.cast_eq_zero, not_false_iff]
· finiteness
_ ≤ ∑ i, μ (s ∩ v i) := by
conv_lhs => rw [A]
apply measure_iUnion_fintype_le
obtain ⟨i, -, hi⟩ : ∃ (i : Fin N), i ∈ Finset.univ ∧ μ s / N ≤ μ (s ∩ v i) :=
by
apply ENNReal.exists_le_of_sum_le _ S
exact ⟨⟨0, bot_lt_iff_ne_bot.2 Npos⟩, Finset.mem_univ _⟩
replace hi : μ s / (N + 1) < μ (s ∩ v i) := by
apply lt_of_lt_of_le _ hi
apply (ENNReal.mul_lt_mul_left hμs.ne' (by finiteness)).2
rw [ENNReal.inv_lt_inv]
conv_lhs => rw [← add_zero (N : ℝ≥0∞)]
exact ENNReal.add_lt_add_left (by finiteness) zero_lt_one
have B : μ (o ∩ v i) = ∑' x : u i, μ (o ∩ closedBall x (r x)) :=
by
have : o ∩ v i = ⋃ (x : s) (_ : x ∈ u i), o ∩ closedBall x (r x) := by simp only [v, inter_iUnion]
rw [this, measure_biUnion (u_count i)]
· exact (hu i).mono fun k => inter_subset_right
· exact fun b _ => omeas.inter measurableSet_closedBall
obtain ⟨w, hw⟩ : ∃ w : Finset (u i), μ s / (N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (x : α) (r (x : α))) :=
by
have C : HasSum (fun x : u i => μ (o ∩ closedBall x (r x))) (μ (o ∩ v i)) := by rw [B];
exact ENNReal.summable.hasSum
have : μ s / (N + 1) < μ (o ∩ v i) := hi.trans_le (measure_mono (inter_subset_inter_left _ so))
exact ((tendsto_order.1 C).1 _ this).exists
refine
⟨Finset.image (fun x : u i => x) w, ?_, ?_, ?_⟩
-- show that the finset is included in `s`.
· simp only [image_subset_iff, Finset.coe_image]
intro y _
simp only [Subtype.coe_prop, mem_preimage]
-- show that it covers a large enough proportion of `s`. For measure computations, we do not
-- use `s` (which might not be measurable), but its measurable superset `o`. Since their measures
-- are the same, this does not spoil the estimates
· suffices H : μ (o \ ⋃ x ∈ w, closedBall (↑x) (r ↑x)) ≤ N / (N + 1) * μ s
by
rw [Finset.set_biUnion_finset_image]
exact le_trans (measure_mono (diff_subset_diff so (Subset.refl _))) H
rw [← diff_inter_self_eq_diff, measure_diff_le_iff_le_add _ inter_subset_right (by finiteness)]
swap
·
exact
.inter (w.nullMeasurableSet_biUnion fun _ _ ↦ measurableSet_closedBall.nullMeasurableSet)
omeas.nullMeasurableSet
calc
μ o = 1 / (N + 1) * μ s + N / (N + 1) * μ s := by
rw [μo, ← add_mul, ENNReal.div_add_div_same, add_comm, ENNReal.div_self, one_mul] <;> simp
_ ≤ μ ((⋃ x ∈ w, closedBall (↑x) (r ↑x)) ∩ o) + N / (N + 1) * μ s :=
by
gcongr
rw [one_div, mul_comm, ← div_eq_mul_inv]
apply hw.le.trans (le_of_eq _)
rw [← Finset.set_biUnion_coe, inter_comm _ o, inter_iUnion₂, Finset.set_biUnion_coe, measure_biUnion_finset]
· have : (w : Set (u i)).PairwiseDisjoint fun b : u i => closedBall (b : α) (r (b : α)) := by intro k _ l _ hkl;
exact hu i k.2 l.2 (Subtype.val_injective.ne hkl)
exact this.mono fun k => inter_subset_right
· intro b _
apply omeas.inter measurableSet_closedBall
· intro k hk l hl hkl
obtain ⟨k', _, rfl⟩ : ∃ k' : u i, k' ∈ w ∧ ↑k' = k := by
simpa only [mem_image, Finset.mem_coe, Finset.coe_image] using hk
obtain ⟨l', _, rfl⟩ : ∃ l' : u i, l' ∈ w ∧ ↑l' = l := by
simpa only [mem_image, Finset.mem_coe, Finset.coe_image] using hl
have k'nel' : (k' : s) ≠ l' := by intro h; rw [h] at hkl; exact hkl rfl
exact hu i k'.2 l'.2 k'nel'
