English
An alternate form of Faulhaber’s theorem for sums of p-th powers: sum over k in Ico 1 n of k^p equals a Bernoulli' expression in p and n.
Русский
Альтернативная форма формулы Фаульхера для сумм степеней p: сумма k^p от k=1 до n равна выражению через Bernoulli'.
LaTeX
$$$\sum_{k \in \mathrm{Ico}\, 1\,(n+1)} k^p = \sum_{i=0}^{p} bernoulli' i \binom{p+1}{i} n^{p+1-i}/(p+1)$$$
Lean4
/-- **Faulhaber's theorem** relating the **sum of p-th powers** to the Bernoulli numbers:
$$\sum_{k=0}^{n-1} k^p = \sum_{i=0}^p B_i\binom{p+1}{i}\frac{n^{p+1-i}}{p+1}.$$
See https://proofwiki.org/wiki/Faulhaber%27s_Formula and [orosi2018faulhaber] for
the proof provided here. -/
theorem sum_range_pow (n p : ℕ) :
(∑ k ∈ range n, (k : ℚ) ^ p) =
∑ i ∈ range (p + 1), bernoulli i * ((p + 1).choose i) * (n : ℚ) ^ (p + 1 - i) / (p + 1) :=
by
have hne : ∀ m : ℕ, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m
have h_cauchy :
((mk fun p => bernoulli p / p !) * mk fun q => coeff (q + 1) (exp ℚ ^ n)) =
mk fun p => ∑ i ∈ range (p + 1), bernoulli i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1)! :=
by
ext q : 1
let f a b :=
bernoulli a / a ! *
coeff (b + 1)
(exp ℚ ^ n)
-- key step: use `PowerSeries.coeff_mul` and then rewrite sums
simp only [f, coeff_mul, coeff_mk, sum_antidiagonal_eq_sum_range_succ f]
apply sum_congr rfl
intro m h
simp only [exp_pow_eq_rescale_exp, rescale, RingHom.coe_mk]
-- manipulate factorials and binomial coefficients
have h : m < q + 1 := by simpa using h
rw [choose_eq_factorial_div_factorial h.le, eq_comm, div_eq_iff (hne q.succ), succ_eq_add_one,
mul_assoc _ _ (q.succ ! : ℚ), mul_comm _ (q.succ ! : ℚ), ← mul_assoc, div_mul_eq_mul_div]
simp only [MonoidHom.coe_mk, OneHom.coe_mk, coeff_exp, Algebra.algebraMap_self, one_div, map_inv₀, map_natCast,
coeff_mk]
rw [mul_comm ((n : ℚ) ^ (q - m + 1)), ← mul_assoc _ _ ((n : ℚ) ^ (q - m + 1)), ← one_div, mul_one_div, div_div,
tsub_add_eq_add_tsub (le_of_lt_succ h), cast_div, cast_mul]
· ring
· exact factorial_mul_factorial_dvd_factorial h.le
·
simp [factorial_ne_zero]
-- same as our goal except we pull out `p!` for convenience
have hps :
(∑ k ∈ range n, (k : ℚ) ^ p) =
(∑ i ∈ range (p + 1), bernoulli i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1)!) * p ! :=
by
suffices
(mk fun p => ∑ k ∈ range n, (k : ℚ) ^ p * algebraMap ℚ ℚ p !⁻¹) =
mk fun p => ∑ i ∈ range (p + 1), bernoulli i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1)!
by
rw [← div_eq_iff (hne p), div_eq_mul_inv, sum_mul]
rw [PowerSeries.ext_iff] at this
simpa using this p
have hexp : exp ℚ - 1 ≠ 0 := by
simp only [exp, PowerSeries.ext_iff, Ne, not_forall]
use 1
simp
have h_r : exp ℚ ^ n - 1 = X * mk fun p => coeff (p + 1) (exp ℚ ^ n) :=
by
have h_const : C (constantCoeff (exp ℚ ^ n)) = 1 := by simp
rw [← h_const, sub_const_eq_X_mul_shift]
-- key step: a chain of equalities of power series
rw [← mul_right_inj' hexp, mul_comm]
rw [← exp_pow_sum, geom_sum_mul, h_r, ← bernoulliPowerSeries_mul_exp_sub_one, bernoulliPowerSeries, mul_right_comm]
simp only [mul_comm, mul_eq_mul_left_iff, hexp, or_false]
refine Eq.trans (mul_eq_mul_right_iff.mpr ?_) (Eq.trans h_cauchy ?_)
· left
congr
·
simp only [mul_comm, factorial]
-- massage `hps` into our goal
rw [hps, sum_mul]
refine sum_congr rfl fun x _ => ?_
simp [field, factorial]
