English
For every n, the sum ∑_{k=0}^{n} (n+1 choose k) bernoulli k equals (n+1) X^n, i.e., the monomial of degree n with coefficient n+1.
Русский
Для каждого n сумма ∑_{k=0}^{n} C(n+1,k) B_k(X) равна (n+1) X^n.
LaTeX
$$$\sum_{k=0}^{n} \binom{n+1}{k} bernoulli k = monomial n (n+1)$$$
Lean4
@[simp]
theorem sum_bernoulli (n : ℕ) : (∑ k ∈ range n, (n.choose k : ℚ) * bernoulli k) = if n = 1 then 1 else 0 := by
cases n with
| zero => simp
| succ n =>
cases n with
| zero => simp
| succ
n =>
suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2
by
simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right, mul_one,
choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
ring
have f := sum_bernoulli' n.succ.succ
simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f
refine Eq.trans ?_ (Eq.trans f ?_)
· congr
funext x
rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]
· simp only [one_div, mul_one, bernoulli'_zero, choose_zero_right, zero_add, choose_one_right, cast_succ,
bernoulli'_one, one_div]
ring
