English
Assuming s avoids all negative integers, and either a ≠ 0 or s ≠ 1, the even part of the Hurwitz zeta satisfies an explicit expression in terms of cosZeta and Gamma functions: hurwitzZetaEven(a,1−s) = 2 (2π)^{−s} Γ(s) cos(π s/2) cosZeta(a,s).
Русский
Пусть s не принимает значения −n (n∈ℕ), и либо a ≠ 0, либо s ≠ 1. Тогда четная часть Hurwitz zeta равна явному выражению через cosZeta и Γ: hurwitzZetaEven(a,1−s) = 2 (2π)^{−s} Γ(s) cos(π s/2) cosZeta(a,s).
LaTeX
$$$$\\text{If } (\\forall n\\in\\mathbb{N},\, s\\neq -n) \\text{ and } (a\\neq 0 \\lor s\\neq 1),$$\n$$\\ \\hurwitzZetaEven(a,1-s) = 2 \\cdot (2\\pi)^{-s} \\Gamma(s) \\cos(\\tfrac{\\pi s}{2}) \\cosZeta(a,s).$$$$
Lean4
/-- If `s` is not in `-ℕ`, and either `a ≠ 0` or `s ≠ 1`, then
`hurwitzZetaEven a (1 - s)` is an explicit multiple of `cosZeta s`. -/
theorem hurwitzZetaEven_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -n) (hs' : a ≠ 0 ∨ s ≠ 1) :
hurwitzZetaEven a (1 - s) = 2 * (2 * π) ^ (-s) * Gamma s * cos (π * s / 2) * cosZeta a s :=
by
have : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (Gammaℝ (1 - s))⁻¹ :=
by
rw [hurwitzZetaEven_def_of_ne_or_ne, div_eq_mul_inv]
simpa [sub_eq_zero, eq_comm (a := s)] using hs'
rw [this, completedHurwitzZetaEven_one_sub, inv_Gammaℝ_one_sub hs, cosZeta,
Function.update_of_ne (by simpa using hs 0), ← Gammaℂ]
generalize Gammaℂ s * cos (π * s / 2) = A
ring_nf
