English
For all k ∈ ℕ, ζ(−k) = −Bernoulli'(k+1)/(k+1).
Русский
Для всех k ∈ ℕ, ζ(−k) = −Bernoulli'(k+1)/(k+1).
LaTeX
$$$$ \operatorname{riemannZeta}(-k) = -\frac{\mathrm{bernoulli}'(k+1)}{k+1}. $$$$
Lean4
/-- Value of Riemann zeta at `-ℕ` in terms of `bernoulli'`. -/
theorem riemannZeta_neg_nat_eq_bernoulli' (k : ℕ) : riemannZeta (-k) = -bernoulli' (k + 1) / (k + 1) :=
by
rcases eq_or_ne k 0 with rfl | hk
·
rw [Nat.cast_zero, neg_zero, riemannZeta_zero, zero_add, zero_add, div_one, bernoulli'_one, Rat.cast_div,
Rat.cast_one, Rat.cast_ofNat, neg_div]
·
rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk (left_mem_Icc.mpr zero_le_one),
ofReal_zero, Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one,
Rat.smul_one_eq_cast, div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]
