English
The Bernoulli' numbers satisfy the recurrence: for all n, the sum ∑_{k=0}^{n-1} binom(n,k) B'(k) equals n (over rationals).
Русский
Числа Бернулли' удовлетворяют рекуррентности: для всех n сумма ∑_{k=0}^{n-1} binom(n,k) B'(k) равна n.
LaTeX
$$$\forall n \in \mathbb{N}, \; \sum_{k=0}^{n-1} {n \choose k} \; \bernoulli'(k) = n$$$
Lean4
@[simp]
theorem sum_bernoulli' (n : ℕ) : (∑ k ∈ range n, (n.choose k : ℚ) * bernoulli' k) = n := by
cases n with
| zero => simp
| succ
n =>
suffices
((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
by
rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
ring
simp_rw [mul_sum, ← mul_assoc]
refine sum_congr rfl fun k hk => ?_
congr
have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast
simp only [← cast_sub (mem_range.1 hk).le, succ_eq_add_one, field, mul_comm]
rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]
