English
If s has density one at x with respect to closed balls, then for any measurable t with μ t ≠ 0 and μ t ≠ ∞, the density of s in {x} + r t relative to {x} + r t tends to 1 as r → 0+.
Русский
Если в точке x множество s имеет плотность единицу по отношению к замкнутым шарам, то для любого измеримого t с μ t ≠ 0 и μ t ≠ ∞ плотность s в {x} + r t по отношению к {x} + r t стремится к 1 при r → 0+.
LaTeX
$$$\displaystyle \lim_{r \to 0^+} \frac{\mu\bigl(s \cap (\{x\} + r\, t)\bigr)}{\mu\bigl(\{x\} + r\, t\bigr)} = 1$$$
Lean4
theorem tendsto_addHaar_inter_smul_one_of_density_one_aux (s : Set E) (hs : MeasurableSet s) (x : E)
(h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)) (t : Set E)
(ht : MeasurableSet t) (h't : μ t ≠ 0) (h''t : μ t ≠ ∞) :
Tendsto (fun r : ℝ => μ (s ∩ ({ x } + r • t)) / μ ({ x } + r • t)) (𝓝[>] 0) (𝓝 1) :=
by
have I : ∀ u v, μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u :=
by
intro u v uzero utop vmeas
simp_rw [div_eq_mul_inv]
rw [← ENNReal.sub_mul]; swap
· simp only [uzero, ENNReal.inv_eq_top, imp_true_iff, Ne, not_false_iff]
congr 1
rw [inter_comm _ u, inter_comm _ u, eq_comm]
exact ENNReal.eq_sub_of_add_eq' utop (measure_inter_add_diff u vmeas)
have L : Tendsto (fun r => μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0) :=
by
have A : Tendsto (fun r => μ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1) :=
by
apply tendsto_const_nhds.congr' _
filter_upwards [self_mem_nhdsWithin]
intro r hr
rw [div_eq_mul_inv, ENNReal.mul_inv_cancel]
· exact (measure_closedBall_pos μ _ hr).ne'
· exact measure_closedBall_lt_top.ne
have B := ENNReal.Tendsto.sub A h (Or.inl ENNReal.one_ne_top)
simp only [tsub_self] at B
apply B.congr' _
filter_upwards [self_mem_nhdsWithin]
rintro r (rpos : 0 < r)
convert I (closedBall x r) sᶜ (measure_closedBall_pos μ _ rpos).ne' measure_closedBall_lt_top.ne hs.compl
rw [compl_compl]
have L' : Tendsto (fun r : ℝ => μ (sᶜ ∩ ({ x } + r • t)) / μ ({ x } + r • t)) (𝓝[>] 0) (𝓝 0) :=
tendsto_addHaar_inter_smul_zero_of_density_zero μ sᶜ x L t ht h''t
have L'' : Tendsto (fun r : ℝ => μ ({ x } + r • t) / μ ({ x } + r • t)) (𝓝[>] 0) (𝓝 1) :=
by
apply tendsto_const_nhds.congr' _
filter_upwards [self_mem_nhdsWithin]
rintro r (rpos : 0 < r)
rw [addHaar_singleton_add_smul_div_singleton_add_smul μ rpos.ne', ENNReal.div_self h't h''t]
have := ENNReal.Tendsto.sub L'' L' (Or.inl ENNReal.one_ne_top)
simp only [tsub_zero] at this
apply this.congr' _
filter_upwards [self_mem_nhdsWithin]
rintro r (rpos : 0 < r)
refine I ({ x } + r • t) s ?_ ?_ hs
·
simp only [h't, abs_of_nonneg rpos.le, pow_pos rpos, addHaar_smul, image_add_left, ENNReal.ofReal_eq_zero, not_le,
or_false, Ne, measure_preimage_add, abs_pow, singleton_add, mul_eq_zero]
·
simp [h''t, ENNReal.ofReal_ne_top, addHaar_smul, image_add_left, ENNReal.mul_eq_top, Ne, measure_preimage_add,
singleton_add]
