English
For real a and s with Re(s) > 1, there is a HasSum expansion for completedHurwitzZetaEven a s as a Dirichlet-like series over ℤ with terms 1/(|n+a|^s)/2 multiplied by Gamma(s).
Русский
Для вещественного a и s с Re(s) > 1 существует разложение HasSum для completedHurwitzZetaEven(a,s) как ряд Дирихле по n ∈ ℤ с членами Γ(s)/(|n+a|^s)/2.
LaTeX
$$$\\forall a\\in\\mathbb{R},\\ {s\\in\\mathbb{C}}\\ (\\Re s>1)\\Rightarrow HasSum\\Bigl(n\\in\\mathbb{Z}\\mapsto \\frac{\\Gamma(s)}{( |n+a|)^{s}}/2\\Bigr)\\bigl(\\mathrm{completedHurwitzZetaEven}(a,s)\\bigr).$$$
Lean4
/-- The even part of the Hurwitz zeta function, i.e. the meromorphic function of `s` which agrees
with `1 / 2 * ∑' (n : ℤ), 1 / |n + a| ^ s` for `1 < re s` -/
noncomputable def hurwitzZetaEven (a : UnitAddCircle) :=
Function.update (fun s ↦ completedHurwitzZetaEven a s / Gammaℝ s) 0 (if a = 0 then -1 / 2 else 0)
