English
A variant of the Faulhaber-type sum: the weighted sum of Bernoulli polynomials with binomial coefficients yields the monomial in X of degree n with coefficient n+1.
Русский
Вариант формулы Фаульхарa: взвешенная сумма Бернулли-полиномов дает многочлен вида (n+1) X^n.
LaTeX
$$$\sum_{k=0}^{n} {n+1 \choose k} bernoulli k = monomial n (n+1)$$$
Lean4
theorem bernoulli_spec' (n : ℕ) :
(∑ k ∈ antidiagonal n, ((k.1 + k.2).choose k.2 : ℚ) / (k.2 + 1) * bernoulli k.1) = if n = 0 then 1 else 0 := by
cases n with
| zero => simp
| succ
n =>
rw [if_neg (succ_ne_zero _)]
-- algebra facts
have h₁ : (1, n) ∈ antidiagonal n.succ := by simp [mem_antidiagonal, add_comm]
have h₂ : (n : ℚ) + 1 ≠ 0 := by norm_cast
have h₃ : (1 + n).choose n = n + 1 := by
simp [add_comm]
-- key equation: the corresponding fact for `bernoulli'`
have H := bernoulli'_spec' n.succ
rw [sum_eq_add_sum_diff_singleton h₁] at H ⊢
apply add_eq_of_eq_sub'
convert eq_sub_of_add_eq' H using 1
· refine sum_congr rfl fun p h => ?_
obtain ⟨h', h''⟩ : p ∈ _ ∧ p ≠ _ := by rwa [mem_sdiff, mem_singleton] at h
simp [bernoulli_eq_bernoulli'_of_ne_one ((not_congr (antidiagonal_congr h' h₁)).mp h'')]
· simp [field, h₃]
norm_num
