Theorems · Theorem · number theory

HurwitzZeta.sinZeta_two_mul_nat_add_one

∀ {k : ℕ} {x : ℝ},
  k ≠ 0 →
    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.

Defined in

Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Cited by

1 results in Mathlib

Foundations

Depth 306 from the axioms · uses propext, Classical.choice, Quot.sound