English
A variant form of Faulhaber’s theorem for sums of p-th powers over Ico; expresses the same identity in another indexing convention.
Русский
Вариант формы формулы Фаульхера для сумм степеней p над Ico; выражение той же формулы в другой индексации.
LaTeX
$$$\sum_{k \in Ico 1\,(n+1)} k^p = \sum_{i=0}^{p} bernoulli' i \binom{p+1}{i} n^{p+1-i}/(p+1)$$$
Lean4
/-- Alternate form of **Faulhaber's theorem**, relating the sum of p-th powers to the Bernoulli
numbers: $$\sum_{k=1}^{n} k^p = \sum_{i=0}^p (-1)^iB_i\binom{p+1}{i}\frac{n^{p+1-i}}{p+1}.$$
Deduced from `sum_range_pow`. -/
theorem sum_Ico_pow (n p : ℕ) :
(∑ k ∈ Ico 1 (n + 1), (k : ℚ) ^ p) =
∑ i ∈ range (p + 1), bernoulli' i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1) :=
by
rw [← Nat.cast_succ]
-- dispose of the trivial case
cases p with
| zero => simp
| succ p =>
let f i := bernoulli i * p.succ.succ.choose i * (n : ℚ) ^ (p.succ.succ - i) / p.succ.succ
let f' i := bernoulli' i * p.succ.succ.choose i * (n : ℚ) ^ (p.succ.succ - i) / p.succ.succ
suffices (∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ) = ∑ i ∈ range p.succ.succ, f' i by convert this
have hle := Nat.le_add_left 1 n
have hne : (p + 1 + 1 : ℚ) ≠ 0 := by norm_cast
have h1 : ∀ r : ℚ, r * (p + 1 + 1) * (n : ℚ) ^ p.succ / (p + 1 + 1 : ℚ) = r * (n : ℚ) ^ p.succ := fun r => by
rw [mul_div_right_comm, mul_div_cancel_right₀ _ hne]
have h2 : f 1 + (n : ℚ) ^ p.succ = 1 / 2 * (n : ℚ) ^ p.succ :=
by
simp_rw [f, bernoulli_one, choose_one_right, succ_sub_succ_eq_sub, cast_succ, tsub_zero, h1]
ring
have :
(∑ i ∈ range p, bernoulli (i + 2) * (p + 2).choose (i + 2) * (n : ℚ) ^ (p - i) / ↑(p + 2)) =
∑ i ∈ range p, bernoulli' (i + 2) * (p + 2).choose (i + 2) * (n : ℚ) ^ (p - i) / ↑(p + 2) :=
sum_congr rfl fun i _ => by rw [bernoulli_eq_bernoulli'_of_ne_one (succ_succ_ne_one i)]
calc
(∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ)
_ = ∑ k ∈ range n.succ, (k : ℚ) ^ p.succ := by
simp [sum_Ico_eq_sub _ hle]
-- extract the last term of the sum
_ = (∑ k ∈ range n, (k : ℚ) ^ p.succ) + (n : ℚ) ^ p.succ := by
rw [sum_range_succ]
-- apply the key lemma, `sum_range_pow`
_ = (∑ i ∈ range p.succ.succ, f i) + (n : ℚ) ^ p.succ := by
simp [f, sum_range_pow]
-- extract the first two terms of the sum
_ = (∑ i ∈ range p, f i.succ.succ) + f 1 + f 0 + (n : ℚ) ^ p.succ := by simp_rw [sum_range_succ']
_ = (∑ i ∈ range p, f i.succ.succ) + (f 1 + (n : ℚ) ^ p.succ) + f 0 := by ring
_ = (∑ i ∈ range p, f i.succ.succ) + 1 / 2 * (n : ℚ) ^ p.succ + f 0 := by
rw [h2]
-- convert from `bernoulli` to `bernoulli'`
_ = (∑ i ∈ range p, f' i.succ.succ) + f' 1 + f' 0 := by
simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]
-- rejoin the first two terms of the sum
_ = ∑ i ∈ range p.succ.succ, f' i := by simp_rw [sum_range_succ']
