English
If s has density zero at x with respect to closed balls, then for any measurable t with μ t ≠ ∞, the density of s in the set {x} + r t relative to {x} + r t tends to 0 as r → 0+ (i.e., the proportion of points from s in the dilated copy shrinks to 0).
Русский
Если у множества s в точке x плотность ноль по отношению к замкнутым шарам, то для любого измеримого t с μ t ≠ ∞ доля точек из s внутри множества {x} + r t по отношению к μ({x} + r t) стремится к нулю при r → 0+.
LaTeX
$$$\displaystyle \lim_{r \to 0^+} \frac{\mu\bigl(s \cap (\{x\} + r\, t)\bigr)}{\mu\bigl(\{x\} + r\, t\bigr)} = 0$$$
Lean4
/-- Consider a point `x` at which a set `s` has density zero, with respect to closed balls. Then it
also has density zero with respect to any measurable set `t`: the proportion of points in `s`
belonging to a rescaled copy `{x} + r • t` of `t` tends to zero as `r` tends to zero. -/
theorem tendsto_addHaar_inter_smul_zero_of_density_zero (s : Set E) (x : E)
(h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)) (t : Set E)
(ht : MeasurableSet t) (h''t : μ t ≠ ∞) :
Tendsto (fun r : ℝ => μ (s ∩ ({ x } + r • t)) / μ ({ x } + r • t)) (𝓝[>] 0) (𝓝 0) :=
by
refine tendsto_order.2 ⟨fun a' ha' => (ENNReal.not_lt_zero ha').elim, fun ε (εpos : 0 < ε) => ?_⟩
rcases eq_or_ne (μ t) 0 with (h't | h't)
· filter_upwards with r
suffices H : μ (s ∩ ({ x } + r • t)) = 0 by rw [H]; simpa only [ENNReal.zero_div] using εpos
apply le_antisymm _ (zero_le _)
calc
μ (s ∩ ({ x } + r • t)) ≤ μ ({ x } + r • t) := measure_mono inter_subset_right
_ = 0 := by simp only [h't, addHaar_smul, image_add_left, measure_preimage_add, singleton_add, mul_zero]
obtain ⟨n, npos, hn⟩ : ∃ n : ℕ, 0 < n ∧ μ (t \ closedBall 0 n) < ε / 2 * μ t :=
by
have A : Tendsto (fun n : ℕ => μ (t \ closedBall 0 n)) atTop (𝓝 (μ (⋂ n : ℕ, t \ closedBall 0 n))) :=
by
have N : ∃ n : ℕ, μ (t \ closedBall 0 n) ≠ ∞ := ⟨0, ((measure_mono diff_subset).trans_lt h''t.lt_top).ne⟩
refine
tendsto_measure_iInter_atTop (fun n ↦ (ht.diff measurableSet_closedBall).nullMeasurableSet) (fun m n hmn ↦ ?_) N
exact diff_subset_diff Subset.rfl (closedBall_subset_closedBall (Nat.cast_le.2 hmn))
have : ⋂ n : ℕ, t \ closedBall 0 n = ∅ := by
simp_rw [diff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl, iUnion_closedBall_nat, compl_univ,
inter_empty]
simp only [this, measure_empty] at A
have I : 0 < ε / 2 * μ t := ENNReal.mul_pos (ENNReal.half_pos εpos.ne').ne' h't
exact (Eventually.and (Ioi_mem_atTop 0) ((tendsto_order.1 A).2 _ I)).exists
have L : Tendsto (fun r : ℝ => μ (s ∩ ({ x } + r • (t ∩ closedBall 0 n))) / μ ({ x } + r • t)) (𝓝[>] 0) (𝓝 0) :=
tendsto_addHaar_inter_smul_zero_of_density_zero_aux2 μ s x h _ t h't n (Nat.cast_pos.2 npos) inter_subset_right
filter_upwards [(tendsto_order.1 L).2 _ (ENNReal.half_pos εpos.ne'), self_mem_nhdsWithin]
rintro r hr (rpos : 0 < r)
have I :
μ (s ∩ ({ x } + r • t)) ≤ μ (s ∩ ({ x } + r • (t ∩ closedBall 0 n))) + μ ({ x } + r • (t \ closedBall 0 n)) :=
calc
μ (s ∩ ({ x } + r • t)) = μ (s ∩ ({ x } + r • (t ∩ closedBall 0 n)) ∪ s ∩ ({ x } + r • (t \ closedBall 0 n))) :=
by rw [← inter_union_distrib_left, ← add_union, ← smul_set_union, inter_union_diff]
_ ≤ μ (s ∩ ({ x } + r • (t ∩ closedBall 0 n))) + μ (s ∩ ({ x } + r • (t \ closedBall 0 n))) :=
(measure_union_le _ _)
_ ≤ μ (s ∩ ({ x } + r • (t ∩ closedBall 0 n))) + μ ({ x } + r • (t \ closedBall 0 n)) := by gcongr;
apply inter_subset_right
calc
μ (s ∩ ({ x } + r • t)) / μ ({ x } + r • t) ≤
(μ (s ∩ ({ x } + r • (t ∩ closedBall 0 n))) + μ ({ x } + r • (t \ closedBall 0 n))) / μ ({ x } + r • t) :=
by gcongr
_ < ε / 2 + ε / 2 := by
rw [ENNReal.add_div]
apply ENNReal.add_lt_add hr _
rwa [addHaar_singleton_add_smul_div_singleton_add_smul μ rpos.ne', ENNReal.div_lt_iff (Or.inl h't) (Or.inl h''t)]
_ = ε := ENNReal.add_halves _
