English
For hk ≠ 0 and x ∈ [0,1], hurwitzZetaEven(x, 1 − 2k) equals −1/(2k) times the Bernoulli polynomial of degree 2k evaluated at x, i.e. the Bernoulli polynomial term expressed from hurwitzZetaEven.
Русский
Для hk ≠ 0 и x ∈ [0,1], hurwitzZetaEven(x, 1 − 2k) = −1/(2k) B_{2k}(x).
LaTeX
$$$$ \mathrm{hurwitzZetaEven}(x,1-2k) = -\frac{1}{2k} \left( (\mathsf{bernoulli}(2k)).map(x) \right). $$$$
Lean4
theorem hurwitzZetaEven_one_sub_two_mul_nat (hk : k ≠ 0) (hx : x ∈ Icc (0 : ℝ) 1) :
hurwitzZetaEven x (1 - 2 * k) = -1 / (2 * k) * ((Polynomial.bernoulli (2 * k)).map (algebraMap ℚ ℂ)).eval (x : ℂ) :=
by
have h1 (n : ℕ) : (2 * k : ℂ) ≠ -n :=
by
rw [← Int.cast_ofNat, ← Int.cast_natCast, ← Int.cast_mul, ← Int.cast_natCast n, ← Int.cast_neg, Ne, Int.cast_inj, ←
Ne]
refine ne_of_gt ((neg_nonpos_of_nonneg n.cast_nonneg).trans_lt (mul_pos two_pos ?_))
exact Nat.cast_pos.mpr (Nat.pos_of_ne_zero hk)
have h2 : (2 * k : ℂ) ≠ 1 := by norm_cast; simp
have h3 : Gammaℂ (2 * k) ≠ 0 :=
by
refine mul_ne_zero (mul_ne_zero two_ne_zero ?_) (Gamma_ne_zero h1)
simp [pi_ne_zero]
rw [hurwitzZetaEven_one_sub _ h1 (Or.inr h2), ← Gammaℂ, cosZeta_two_mul_nat' hk hx, ← mul_assoc, ← mul_div_assoc,
mul_assoc, mul_div_cancel_left₀ _ h3, ← mul_div_assoc]
congr 2
rw [mul_div_assoc, mul_div_cancel_left₀ _ two_ne_zero, ← ofReal_natCast, ← ofReal_mul, ← ofReal_cos, mul_comm π, ←
sub_zero (k * π), cos_nat_mul_pi_sub, Real.cos_zero, mul_one, ofReal_pow, ofReal_neg, ofReal_one, pow_succ,
mul_neg_one, mul_neg, ← mul_pow, neg_one_mul, neg_neg, one_pow]
