English
For hk ≠ 0 and x ∈ [0,1], sinZeta(x, 2k+1) equals (-1)^{k+1} (2π)^{2k+1} / 2(2k+1)! times the Bernoulli polynomial of order 2k+1 evaluated at x.
Русский
Для hk ≠ 0 и x ∈ [0,1], sinZeta(x, 2k+1) = (-1)^{k+1} (2π)^{2k+1} / (2(2k+1)!) · Bernoulli_{2k+1}(x).
LaTeX
$$$$ \sinZeta(x,2k+1) = (-1)^{k+1} \frac{(2\pi)^{2k+1}}{2\,(2k+1)!} \big( Bernoulli(2k+1) \big)(x). $$$$
Lean4
/-- Reformulation of `sinZeta_two_mul_nat_add_one` using `Gammaℂ`. -/
theorem sinZeta_two_mul_nat_add_one' (hk : k ≠ 0) (hx : x ∈ Icc (0 : ℝ) 1) :
sinZeta x (2 * k + 1) =
(-1) ^ (k + 1) / (2 * k + 1) / Gammaℂ (2 * k + 1) *
((Polynomial.bernoulli (2 * k + 1)).map (algebraMap ℚ ℂ)).eval (x : ℂ) :=
by
rw [sinZeta_two_mul_nat_add_one hk hx]
congr 1
have : (2 * k + 1)! = (2 * k + 1) * Complex.Gamma (2 * k + 1) := by
rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)), Complex.Gamma_nat_eq_factorial, ←
Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul, ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
simp_rw [this, Gammaℂ, cpow_neg, ← div_div, div_inv_eq_mul, div_mul_eq_mul_div, div_div]
rw [(by simp : 2 * (k : ℂ) + 1 = ↑(2 * k + 1)), cpow_natCast]
ring
