English
Values of Hurwitz zeta at negative integers are given by HurwitzZetaNegNat: for k>0, hurwitzZeta(x, −k) equals −1/(k+1) times Bernoulli polynomial of order k+1 evaluated at x.
Русский
Значения HurwitzZeta в отрицательных целых числаx задаются через HurwitzZetaNegNat: для k>0, hurwitzZeta(x, −k) = −1/(k+1) B_{k+1}(x).
LaTeX
$$$$ \mathrm{hurwitzZeta}(x, -k) = -\frac{1}{k+1} \left( (\mathsf{bernoulli}(k+1)).map(x) \right). $$$$
Lean4
/-- Values of Hurwitz zeta functions at (strictly) negative integers.
TODO: This formula is also correct for `k = 0`; but our current proof does not work in this
case. -/
theorem hurwitzZeta_neg_nat (hk : k ≠ 0) (hx : x ∈ Icc (0 : ℝ) 1) :
hurwitzZeta x (-k) = -1 / (k + 1) * ((Polynomial.bernoulli (k + 1)).map (algebraMap ℚ ℂ)).eval (x : ℂ) :=
by
rcases Nat.even_or_odd' k with ⟨n, (rfl | rfl)⟩
· exact_mod_cast hurwitzZeta_neg_two_mul_nat (by cutsat : n ≠ 0) hx
· exact_mod_cast hurwitzZeta_one_sub_two_mul_nat (by cutsat : n + 1 ≠ 0) hx
