English
A reformulation of cosZeta at even integers using Gammaℂ; cosZeta(x, 2k) can be written as a rational expression involving Gammaℂ(2k) and the Bernoulli polynomial.
Русский
Переформулировано кос-зета в четных случаях через Gammaℂ(2k) и Бернулли-полином.
LaTeX
$$$$ \cosZeta(x,2k) = \frac{(-1)^{k+1}}{2k} \frac{1}{\Gammaℂ(2k)} ( (\mathsf{bernoulli}(2k))^{\#} (x) ) $$$$
Lean4
/-- 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 sinZeta_two_mul_nat_add_one (hk : k ≠ 0) (hx : x ∈ Icc 0 1) :
sinZeta x (2 * k + 1) =
(-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / (2 * k + 1)! *
((Polynomial.bernoulli (2 * k + 1)).map (algebraMap ℚ ℂ)).eval (x : ℂ) :=
by
rw [← (hasSum_nat_sinZeta x (?_ : 1 < re (2 * k + 1))).tsum_eq]
· refine Eq.trans ?_ <| (congr_arg ofReal (hasSum_one_div_nat_pow_mul_sin hk hx).tsum_eq).trans ?_
· rw [ofReal_tsum]
refine tsum_congr fun n ↦ ?_
norm_cast
ring_nf
· push_cast
congr 1
have : (Polynomial.bernoulli (2 * k + 1)).map (algebraMap ℚ ℂ) = _ :=
(Polynomial.map_map (algebraMap ℚ ℝ) ofRealHom _).symm
rw [this, ← ofRealHom_eq_coe, ← ofRealHom_eq_coe]
apply Polynomial.map_aeval_eq_aeval_map (by simp)
· norm_cast
cutsat
