English
If f is periodic and behaves near infinity, then f decays exponentially: f = O(exp(-2π im z / h)).
Русский
Если f периодична и ведет себя при бесконечности, то f сокращается экспоненциально: f = O(exp(-2π im z / h)).
LaTeX
$$f =O[I∞] (\, z \mapsto \exp(-2\pi i \operatorname{Im}(z)/h) \,)$$
Lean4
/-- If `f` is periodic, holomorphic near `I∞`, and tends to zero at `I∞`, then in fact it tends to zero
exponentially fast.
-/
theorem exp_decay_of_zero_at_inf (hh : 0 < h) (hf : Periodic f h) (h_hol : ∀ᶠ z in I∞, DifferentiableAt ℂ f z)
(h_zer : ZeroAtFilter I∞ f) : f =O[I∞] fun z ↦ Real.exp (-2 * π * im z / h) :=
by
suffices cuspFunction h f =O[_] id by
simpa only [comp_def, eq_cuspFunction hh.ne' hf, id_eq, norm_qParam] using
(this.comp_tendsto (qParam_tendsto hh)).norm_right
simpa only [cuspFunction_zero_of_zero_at_inf hh h_zer, sub_zero] using
(differentiableAt_cuspFunction_zero hh hf h_hol h_zer.boundedAtFilter).isBigO_sub.mono nhdsWithin_le_nhds
