English
If a ∈ Icc 0 1, there is a HasSum representation for hurwitzZetaEven a s without absolute values, valid in the convergence range.
Русский
Если a ∈ Icc 0 1, существует ряд без модулей, дающий hurwitzZetaEven a s в диапазоне сходимости.
LaTeX
$$$\\forall a\\in Icc(0,1),\\ (\\Re s>1)\\Rightarrow HasSum\\Bigl(n\\mapsto \\frac{1}{(n+a)^s} + \\frac{1}{(n+1-a)^s}\\Bigr)/2\\ (\\mathrm{hurwitzZetaEven}(\\mathrm{mk}(a),s)).$$$
Lean4
/-- Formula for `hurwitzZetaEven` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version without absolute values, assuming `a ∈ Icc 0 1`) -/
theorem hasSum_nat_hurwitzZetaEven_of_mem_Icc {a : ℝ} (ha : a ∈ Icc 0 1) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℕ ↦ (1 / (n + a : ℂ) ^ s + 1 / (n + 1 - a : ℂ) ^ s) / 2) (hurwitzZetaEven a s) :=
by
refine (hasSum_nat_hurwitzZetaEven a hs).congr_fun fun n ↦ ?_
congr 2 <;> rw [abs_of_nonneg (by linarith [ha.1, ha.2])] <;> simp
