English
Let μ be a Haar measure on a finite dimensional real vector space E, and s ⊆ E. If at a point x the density of s inside balls B(x, r) tends to 0 as r ↓ 0, then for any measurable t, u ⊆ E with μ(u) ≠ 0 and any R > 0 such that t is contained in the closed ball around 0 of radius R, the density of s inside the dilated copy {x} + r t, relative to μ({x} + r u), tends to 0 as r ↓ 0.
Русский
Пусть μ — гармонически инвариментная мера на конечномерном вещественном векторном пространстве E, и s ⊆ E. Если в точке x плотность s по отношению к окрестностям B(x, r) стремится к 0 при r → 0+, то для любой измеримой пары t, u ⊆ E с μ(u) ≠ 0 и любого R > 0, при условии t ⊆ closedBall 0 R, плотность s в вытянутом копии {x} + r t относительно μ({x} + r u) стремится к 0 при r → 0+.
LaTeX
$$$\displaystyle \lim_{r \to 0^+} \frac{\mu\bigl(s \cap (\{x\} + r\, t)\bigr)}{\mu\bigl(\{x\} + r\, u\bigr)} = 0$$$
Lean4
theorem tendsto_addHaar_inter_smul_zero_of_density_zero_aux2 (s : Set E) (x : E)
(h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)) (t : Set E) (u : Set E)
(h'u : μ u ≠ 0) (R : ℝ) (Rpos : 0 < R) (t_bound : t ⊆ closedBall 0 R) :
Tendsto (fun r : ℝ => μ (s ∩ ({ x } + r • t)) / μ ({ x } + r • u)) (𝓝[>] 0) (𝓝 0) :=
by
set t' := R⁻¹ • t with ht'
set u' := R⁻¹ • u with hu'
have A : Tendsto (fun r : ℝ => μ (s ∩ ({ x } + r • t')) / μ ({ x } + r • u')) (𝓝[>] 0) (𝓝 0) :=
by
apply tendsto_addHaar_inter_smul_zero_of_density_zero_aux1 μ s x h t' u'
·
simp only [u', h'u, (pow_pos Rpos _).ne', abs_nonpos_iff, addHaar_smul, not_false_iff, ENNReal.ofReal_eq_zero,
inv_eq_zero, inv_pow, Ne, or_self_iff, mul_eq_zero]
· refine (smul_set_mono t_bound).trans_eq ?_
rw [smul_closedBall _ _ Rpos.le, smul_zero, Real.norm_of_nonneg (inv_nonneg.2 Rpos.le), inv_mul_cancel₀ Rpos.ne']
have B : Tendsto (fun r : ℝ => R * r) (𝓝[>] 0) (𝓝[>] (R * 0)) :=
by
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
· exact (tendsto_const_nhds.mul tendsto_id).mono_left nhdsWithin_le_nhds
· filter_upwards [self_mem_nhdsWithin]
intro r rpos
rw [mul_zero]
exact mul_pos Rpos rpos
rw [mul_zero] at B
apply (A.comp B).congr' _
filter_upwards [self_mem_nhdsWithin]
rintro r -
have T : (R * r) • t' = r • t := by rw [mul_comm, ht', smul_smul, mul_assoc, mul_inv_cancel₀ Rpos.ne', mul_one]
have U : (R * r) • u' = r • u := by rw [mul_comm, hu', smul_smul, mul_assoc, mul_inv_cancel₀ Rpos.ne', mul_one]
dsimp
rw [T, U]
