English
At 0, cuspFunction equals the limit under nhdsWithin near 0.
Русский
В точке 0 cuspFunction равна пределy в окрестности 0.
LaTeX
$$cuspFunction(h,f)(0) = limUnder (nhdsWithin 0 (Set.compl {0})) (cuspFunction(h,f))$$
Lean4
/-- If `f` is periodic, and holomorphic and bounded near `I∞`, then it tends to a limit at `I∞`,
and this limit is the value of its cusp function at 0.
-/
theorem tendsto_at_I_inf (hh : 0 < h) (hf : Periodic f h) (h_hol : ∀ᶠ z in I∞, DifferentiableAt ℂ f z)
(h_bd : BoundedAtFilter I∞ f) : Tendsto f I∞ (𝓝 <| cuspFunction h f 0) :=
by
suffices Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 <| cuspFunction h f 0) by
simpa only [Function.comp_def, eq_cuspFunction hh.ne' hf] using this.comp (qParam_tendsto hh)
exact tendsto_nhdsWithin_of_tendsto_nhds (differentiableAt_cuspFunction_zero hh hf h_hol h_bd).continuousAt.tendsto
