English
For real a, there is a HasSum representation of hurwitzZetaEven a s as a double-sum over natural numbers with two reciprocal power terms.
Русский
Для вещественного a существует представление HasSum для hurwitzZetaEven a s как двойная сумма по натовым числам с двумя термами 1/(n+a)^s и 1/(n+1−a)^s.
LaTeX
$$$\\forall a:\\mathbb{R},\\ {s:\\mathbb{C}}\\ (\\Re s>1)\\Rightarrow HasSum\\Bigl(n\\mapsto \\frac{\\mathrm{HDiv}(1, (n+a)^s) + \\mathrm{HDiv}(1, (n+1-a)^s)}{2}\\Bigr)\\ (\\mathrm{hurwitzZetaEven}(\\mathrm{mk}(a),s)).$$$
Lean4
/-- Formula for `hurwitzZetaEven` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version with absolute values) -/
theorem hasSum_nat_hurwitzZetaEven (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℕ ↦ (1 / (↑|n + a| : ℂ) ^ s + 1 / (↑|n + 1 - a| : ℂ) ^ s) / 2) (hurwitzZetaEven a s) :=
by
refine (hasSum_int_hurwitzZetaEven a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_
simp [← abs_neg (n + 1 - a), -neg_sub, neg_sub', add_div]
