English
For every a on the unit circle, the oddKernel(a) has exponential decay at +∞; there exists p>0 such that oddKernel(a)(x) = O(exp(-p x)) as x → ∞.
Русский
Для каждого a на единичном круге oddKernel(a) имеет экспоненциальное затухание при x → +∞; существует p>0, такое что oddKernel(a)(x) = O(e^{-p x}).
LaTeX
$$$$ \exists p>0,\, \operatorname{IsBigO}_{atTop}(\text{oddKernel}(a), x \mapsto e^{-p x}). $$$$
Lean4
/-- The function `oddKernel a` has exponential decay at `+∞`, for any `a`. -/
theorem isBigO_atTop_oddKernel (a : UnitAddCircle) :
∃ p, 0 < p ∧ IsBigO atTop (oddKernel a) (fun x ↦ Real.exp (-p * x)) := by
induction a using QuotientAddGroup.induction_on with
| H b =>
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_one b
refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
filter_upwards [eventually_gt_atTop 0] with t ht
simpa [← (hasSum_int_oddKernel b ht).tsum_eq, HurwitzKernelBounds.F_int, HurwitzKernelBounds.f_int,
abs_of_nonneg (exp_pos _).le] using norm_tsum_le_tsum_norm (hasSum_int_oddKernel b ht).summable.norm
