English
For every a, sinKernel decays exponentially: there exists p>0 with sinKernel(a) = O(exp(-p x)) as x→∞.
Русский
Для каждого a синKernel экспоненциально затухает: существует p>0, такое что sinKernel(a) = O(exp(-p x)) при x→∞.
LaTeX
$$$$ \exists p>0,\; \operatorname{IsBigO}_{atTop}(\sinKernel(a), x \mapsto e^{-p x}). $$$$
Lean4
/-- Formula for `completedSinZeta` as a Dirichlet series in the convergence range
(first version, with sum over `ℤ`). -/
theorem hasSum_int_completedSinZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℤ ↦ Gammaℝ (s + 1) * (-I) * Int.sign n * cexp (2 * π * I * a * n) / (↑|n| : ℂ) ^ s / 2)
(completedSinZeta a s) :=
by
let c (n : ℤ) : ℂ := -I * cexp (2 * π * I * a * n) / 2
have hc (n : ℤ) : ‖c n‖ = 1 / 2 := by
simp_rw [c,
(by { push_cast; ring
} : 2 * π * I * a * n = ↑(2 * π * a * n) * I),
norm_div, RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]
have hF t (ht : 0 < t) : HasSum (fun n ↦ c n * n * rexp (-π * n ^ 2 * t)) (sinKernel a t / 2) :=
by
refine ((hasSum_int_sinKernel a ht).div_const 2).congr_fun fun n ↦ ?_
rw [div_mul_eq_mul_div, div_mul_eq_mul_div, mul_right_comm (-I)]
have h_sum : Summable fun i ↦ ‖c i‖ / |↑i| ^ s.re :=
by
simp_rw [hc, div_right_comm]
apply Summable.div_const
apply Summable.of_nat_of_neg <;> simpa
refine (mellin_div_const .. ▸ hasSum_mellin_pi_mul_sq' (zero_lt_one.trans hs) hF h_sum).congr_fun fun n ↦ ?_
simp [Int.sign_eq_sign, ← Int.cast_abs] -- non-terminal simp OK when `ring` follows
ring
