English
The cosKernel is even in its first argument, i.e., cosKernel(-a, t) = cosKernel(a, t).
Русский
cosKernel по первому аргументу чётна: cosKernel(-a,t) = cosKernel(a,t).
LaTeX
$$$$ \\cosKernel(-a,t) = \\cosKernel(a,t). $$$$
Lean4
/-- The function `cosKernel a - 1` has exponential decay at `+∞`, for any `a`. -/
theorem isBigO_atTop_cosKernel_sub (a : UnitAddCircle) :
∃ p, 0 < p ∧ IsBigO atTop (cosKernel a · - 1) (fun x ↦ Real.exp (-p * x)) := by
induction a using QuotientAddGroup.induction_on with
| H a =>
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub zero_le_one
refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩
filter_upwards [eventually_gt_atTop 0] with t ht
simp only [eq_false_intro one_ne_zero, if_false, sub_zero, ← (hasSum_nat_cosKernel₀ a ht).tsum_eq,
HurwitzKernelBounds.F_nat]
apply tsum_of_norm_bounded ((HurwitzKernelBounds.summable_f_nat 0 1 ht).hasSum.mul_left 2)
intro n
rw [norm_mul, norm_mul, norm_two, mul_assoc, mul_le_mul_iff_of_pos_left two_pos, norm_of_nonneg (exp_pos _).le,
HurwitzKernelBounds.f_nat, pow_zero, one_mul, Real.norm_eq_abs]
exact mul_le_of_le_one_left (exp_pos _).le (abs_cos_le_one _)
