English
A reformulation of cosZeta_two_mul_nat using Gammaℂ; expresses cosZeta at even integers via Bernoulli and Gammaℂ(2k).
Русский
Переформулировка cosZeta_two_mul_nat через Gammaℂ; выражает cosZeta в четных точках через Бернулли и Gammaℂ(2k).
LaTeX
$$$$ \cosZeta(x,2k) = \frac{(-1)^{k+1}}{(2k)} \frac{1}{\Gammaℂ(2k)} \big( (\mathsf{bernoulli}(2k))\_{{}\mathbb{C}}(x) \big). $$$$
Lean4
/-- Reformulation of `cosZeta_two_mul_nat` using `Gammaℂ`. -/
theorem cosZeta_two_mul_nat' (hk : k ≠ 0) (hx : x ∈ Icc (0 : ℝ) 1) :
cosZeta x (2 * k) =
(-1) ^ (k + 1) / (2 * k) / Gammaℂ (2 * k) * ((Polynomial.bernoulli (2 * k)).map (algebraMap ℚ ℂ)).eval (x : ℂ) :=
by
rw [cosZeta_two_mul_nat hk hx]
congr 1
have : (2 * k)! = (2 * k) * Complex.Gamma (2 * k) := by
rw [(by { norm_cast; omega
} : 2 * (k : ℂ) = ↑(2 * k - 1) + 1),
Complex.Gamma_nat_eq_factorial, ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ,
Nat.sub_add_cancel (by cutsat)]
simp_rw [this, Gammaℂ, cpow_neg, ← div_div, div_inv_eq_mul, div_mul_eq_mul_div, div_div,
mul_right_comm (2 : ℂ) (k : ℂ)]
norm_cast
