English
For real a and s with Re(s) > 1, there is a Dirichlet series representation of completedCosZeta(a,s) as a sum over ℤ involving Gamma(s) and e^{2πia n}.
Русский
Для действительного a и s с Re(s) > 1 существует ряд Дирихле для completedCosZeta(a,s) как сумма по n∈ℤ с Gamma(s) и e^{2π i a n}.
LaTeX
$$$\\forall a\\in\\mathbb{R},\\ {s\\in\\mathbb{C}}\\ (\\Re s>1)\\Rightarrow HasSum\\Bigl(n\\mapsto \\Gamma(s)\\, e^{2\\pi i a n}\\,/\\, (|n|)^{s}\\ /2\\Bigr)\\ (\\mathrm{completedHurwitzZeta}(a,s)).$$$
Lean4
/-- Formula for `completedCosZeta` as a Dirichlet series in the convergence range
(first version, with sum over `ℤ`). -/
theorem hasSum_int_completedCosZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℤ ↦ Gammaℝ s * cexp (2 * π * I * a * n) / (↑|n| : ℂ) ^ s / 2) (completedCosZeta a s) :=
by
let c (n : ℤ) : ℂ := cexp (2 * π * I * a * n) / 2
have hF t (ht : 0 < t) :
HasSum (fun n : ℤ ↦ if n = 0 then 0 else c n * rexp (-π * n ^ 2 * t)) ((cosKernel a t - 1) / 2) :=
by
refine ((hasSum_int_cosKernel₀ a ht).div_const 2).congr_fun fun n ↦ ?_
split_ifs <;> simp [c, div_mul_eq_mul_div]
simp only [← Int.cast_eq_zero (α := ℝ)] at hF
rw [show completedCosZeta a s = mellin (fun t ↦ (cosKernel a t - 1 : ℂ) / 2) (s / 2)
by
rw [mellin_div_const, completedCosZeta]
congr 1
refine ((hurwitzEvenFEPair a).symm.hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm
rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]]
refine (hasSum_mellin_pi_mul_sq (zero_lt_one.trans hs) hF ?_).congr_fun fun n ↦ ?_
· apply (((summable_one_div_int_add_rpow 0 s.re).mpr hs).div_const 2).of_norm_bounded
intro i
simp only [c,
(by { push_cast; ring
} : 2 * π * I * a * i = ↑(2 * π * a * i) * I),
norm_div, RCLike.norm_ofNat, Complex.norm_exp_ofReal_mul_I, add_zero, norm_one,
norm_of_nonneg (by positivity : 0 ≤ |(i : ℝ)| ^ s.re), div_right_comm, le_rfl]
· simp [c, ← Int.cast_abs, div_right_comm, mul_div_assoc]
