Special values of Hurwitz and Riemann zeta functions

This file gives the formula for ζ (2 * k), for k a non-zero integer, in terms of Bernoulli numbers. More generally, we give formulae for any Hurwitz zeta functions at any (strictly) negative integer in terms of Bernoulli polynomials.

(Note that most of the actual work for these formulae is done elsewhere, in Mathlib.NumberTheory.ZetaValues. This file has only those results which really need the definition of Hurwitz zeta and related functions, rather than working directly with the defining sums in the convergence range.)

Main results

• hurwitzZeta_neg_nat: for k : ℕ with k ≠ 0, and any x ∈ ℝ / ℤ, the special value hurwitzZeta x (-k) is equal to -(Polynomial.bernoulli (k + 1) x) / (k + 1).
• riemannZeta_neg_nat_eq_bernoulli : for any k ∈ ℕ we have the formula riemannZeta (-k) = (-1) ^ k * bernoulli (k + 1) / (k + 1)
• riemannZeta_two_mul_nat: formula for ζ(2 * k) for k ∈ ℕ, k ≠ 0 in terms of Bernoulli numbers

TODO

• Extend to cover Dirichlet L-functions.
• The formulae are correct for s = 0 as well, but we do not prove this case, since this requires Fourier series which are only conditionally convergent, which is difficult to approach using the methods in the library at the present time (May 2024).

theorem HurwitzZeta.cosZeta_two_mul_nat {k : ℕ} {x : ℝ} (hk : k ≠ 0) (hx : x ∈ Set.Icc 0 1) : HurwitzZeta.cosZeta (↑x) (2 * ↑k) = (-1) ^ (k + 1) * (2 * ↑Real.pi) ^ (2 * k) / 2 / ↑(2 * k).factorial * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Express the value of cosZeta at a positive even integer as a value of the Bernoulli polynomial.

theorem HurwitzZeta.sinZeta_two_mul_nat_add_one {k : ℕ} {x : ℝ} (hk : k ≠ 0) (hx : x ∈ Set.Icc 0 1) : HurwitzZeta.sinZeta (↑x) (2 * ↑k + 1) = (-1) ^ (k + 1) * (2 * ↑Real.pi) ^ (2 * k + 1) / 2 / ↑(2 * k + 1).factorial * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Express the value of sinZeta at an odd integer > 1 as a value of the Bernoulli polynomial.

Note that this formula is also correct for k = 0 (i.e. for the value at s = 1), but we do not prove it in this case, owing to the additional difficulty of working with series that are only conditionally convergent.

theorem HurwitzZeta.cosZeta_two_mul_nat' {k : ℕ} {x : ℝ} (hk : k ≠ 0) (hx : x ∈ Set.Icc 0 1) : HurwitzZeta.cosZeta (↑x) (2 * ↑k) = (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Reformulation of cosZeta_two_mul_nat using Gammaℂ.

theorem HurwitzZeta.sinZeta_two_mul_nat_add_one' {k : ℕ} {x : ℝ} (hk : k ≠ 0) (hx : x ∈ Set.Icc 0 1) : HurwitzZeta.sinZeta (↑x) (2 * ↑k + 1) = (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Reformulation of sinZeta_two_mul_nat_add_one using Gammaℂ.

theorem HurwitzZeta.hurwitzZetaEven_one_sub_two_mul_nat {k : ℕ} {x : ℝ} (hk : k ≠ 0) (hx : x ∈ Set.Icc 0 1) : HurwitzZeta.hurwitzZetaEven (↑x) (1 - 2 * ↑k) = -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

theorem HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat {k : ℕ} {x : ℝ} (hk : k ≠ 0) (hx : x ∈ Set.Icc 0 1) : HurwitzZeta.hurwitzZetaOdd (↑x) (-(2 * ↑k)) = -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

theorem HurwitzZeta.hurwitzZeta_neg_nat {k : ℕ} {x : ℝ} (hk : k ≠ 0) (hx : x ∈ Set.Icc 0 1) : HurwitzZeta.hurwitzZeta (↑x) (-↑k) = -1 / (↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1)))

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 riemannZeta_two_mul_nat {k : ℕ} (hk : k ≠ 0) : riemannZeta (2 * ↑k) = (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * ↑Real.pi ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k).factorial

Explicit formula for ζ (2 * k), for k ∈ ℕ with k ≠ 0, in terms of the Bernoulli number bernoulli (2 * k).

Compare hasSum_zeta_nat for a version formulated in terms of a sum over 1 / n ^ (2 * k), and riemannZeta_neg_nat_eq_bernoulli for values at negative integers (equivalent to the above via the functional equation).

theorem riemannZeta_two : riemannZeta 2 = ↑Real.pi ^ 2 / 6

theorem riemannZeta_four : riemannZeta 4 = ↑Real.pi ^ 4 / 90

theorem riemannZeta_neg_nat_eq_bernoulli' (k : ℕ) : riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)

Value of Riemann zeta at -ℕ in terms of bernoulli'.

theorem riemannZeta_neg_nat_eq_bernoulli (k : ℕ) : riemannZeta (-↑k) = (-1) ^ k * ↑(bernoulli (k + 1)) / (↑k + 1)

Value of Riemann zeta at -ℕ in terms of bernoulli.