English
In the convergence range Re(s) > 1, the cosine zeta can be written as a Dirichlet series over all integers: HasSum_{n∈ℤ} e^{2π i a n}/(2|n|^s) = cosZeta(a)(s).
Русский
В области сходимости Re(s) > 1 косинусная зета выражается через двойной ряд Дирихле по всем n∈ℤ: HasSum_{n∈ℤ} e^{2π i a n}/(2|n|^s) = cosZeta(a)(s).
LaTeX
$$$$\\text{HasSum}_{n\\in\\mathbb{Z}} \\frac{e^{2\\pi i a n}}{2|n|^s} = \\cosZeta(a)(s), \\quad 1<\\Re(s).$$$$
Lean4
/-- Formula for `cosZeta` as a Dirichlet series in the convergence range, with sum over `ℤ`. -/
theorem hasSum_int_cosZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℤ ↦ cexp (2 * π * I * a * n) / ↑|n| ^ s / 2) (cosZeta a s) :=
by
rw [cosZeta, Function.update_of_ne (ne_zero_of_one_lt_re hs)]
refine ((hasSum_int_completedCosZeta a hs).div_const (Gammaℝ s)).congr_fun fun n ↦ ?_
rw [mul_div_assoc _ (cexp _), div_right_comm _ (2 : ℂ),
mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]
