English
For nonzero k and x ∈ [0,1], cosZeta(x, 2k) equals a Bernoulli-polynomial term: cosZeta(x, 2k) = (-1)^{k+1} (2π)^{2k} / 2/(2k)! times the Bernoulli polynomial (2k) evaluated at x.
Русский
Для ненулевого k и x ∈ [0,1] cosZeta(x, 2k) выражается через Бернулли-полином: cosZeta(x, 2k) = (-1)^{k+1} (2π)^{2k} /(2·(2k)!) Bernoulli_{2k}(x).
LaTeX
$$$$ \cosZeta(x,2k) = (-1)^{k+1} \frac{(2\pi)^{2k}}{2\,(2k)!} \left( (\mathsf{bernoulli}(2k).map) (x) \right). $$$$
Lean4
/-- Express the value of `cosZeta` at a positive even integer as a value
of the Bernoulli polynomial. -/
theorem cosZeta_two_mul_nat (hk : k ≠ 0) (hx : x ∈ Icc 0 1) :
cosZeta x (2 * k) =
(-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / (2 * k)! *
((Polynomial.bernoulli (2 * k)).map (algebraMap ℚ ℂ)).eval (x : ℂ) :=
by
rw [← (hasSum_nat_cosZeta x (?_ : 1 < re (2 * k))).tsum_eq]
· refine Eq.trans ?_ <| (congr_arg ofReal (hasSum_one_div_nat_pow_mul_cos 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)).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
