English
For real a and s with Re(s) > 1, has-sum for hurwitzZetaEven (real a) s holds with a sum of two HDiv terms over n.
Русский
Для вещественного a и s с Re(s) > 1 имеет место ряд для hurwitzZetaEven(a,s) в виде суммы из двух членов по n.
LaTeX
$$$\\forall a:\\mathbb{R},\\ {s:\\mathbb{C}}\\ (\\Re s>1)\\Rightarrow HasSum\\Bigl(n\\mapsto \\mathrm{HDiv}(1, (|n+a|)^s) + \\mathrm{HDiv}(1, (|n+1-a|)^s)\\Bigr)\\ (\\mathrm{hurwitzZetaEven}(\\mathrm{mk}(a),s)).$$$
Lean4
/-- Formula for `hurwitzZetaEven` as a Dirichlet series in the convergence range, with sum over `ℤ`.
-/
theorem hasSum_int_hurwitzZetaEven (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℤ ↦ 1 / (↑|n + a| : ℂ) ^ s / 2) (hurwitzZetaEven a s) :=
by
rw [hurwitzZetaEven, Function.update_of_ne (ne_zero_of_one_lt_re hs)]
have := (hasSum_int_completedHurwitzZetaEven a hs).div_const (Gammaℝ s)
exact
this.congr_fun fun n ↦ by
simp only [div_right_comm _ _ (Gammaℝ _), div_self (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]
