English
If h > 0, the function qParam(h, z) tends to 0 as z tends to infinity in the sense of the nhdsWithin of infinity excluding 0.
Русский
Если h > 0, то qParam(h, z) стремится к 0, когда z tends к бесконечности по отношению nhdsWithin, исключая 0.
LaTeX
$$hh > 0 ⇒ Tendsto (qParam h) I∞ (𝓝[≠] 0)$$
Lean4
theorem qParam_tendsto (hh : 0 < h) : Tendsto (qParam h) I∞ (𝓝[≠] 0) :=
by
refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_ (.of_forall fun q ↦ exp_ne_zero _)
rw [tendsto_zero_iff_norm_tendsto_zero]
simp only [norm_qParam]
apply (tendsto_comap'_iff (m := fun y ↦ Real.exp (-2 * π * y / h)) (range_im ▸ univ_mem)).mpr
refine Real.tendsto_exp_atBot.comp (.atBot_div_const hh (tendsto_id.const_mul_atTop_of_neg ?_))
simpa using Real.pi_pos
