English
Another version of Faulhaber’s theorem in terms of Bernoulli numbers with sum over range n.
Русский
Еще одна версия теоремы Фаульхера через числа Бернулли с суммой по диапазону n.
LaTeX
$$((p+1) ∑ k ∈ range n) = bernoulli(p.succ).eval(n) − bernoulli(p.succ)$$
Lean4
/-- Another version of `sum_range_pow`. -/
theorem sum_range_pow_eq_bernoulli_sub (n p : ℕ) :
((p + 1 : ℚ) * ∑ k ∈ range n, (k : ℚ) ^ p) = (bernoulli p.succ).eval (n : ℚ) - _root_.bernoulli p.succ :=
by
rw [sum_range_pow, bernoulli_def, eval_finset_sum, ← sum_div, mul_div_cancel₀ _ _]
· simp_rw [eval_monomial]
symm
rw [← sum_flip _, sum_range_succ]
simp only [tsub_self, tsub_zero, choose_zero_right, cast_one, mul_one, _root_.pow_zero, add_tsub_cancel_right]
apply sum_congr rfl fun x hx => _
intro x hx
apply congr_arg₂ _ (congr_arg₂ _ _ _) rfl
· rw [Nat.sub_sub_self (mem_range_le hx)]
· rw [← choose_symm (mem_range_le hx)]
· norm_cast
