bernoulli_succ_eval — Mathlib

English

An alternate Faulhaber formula: B_{p+1}(n) = B_{p+1} + (p+1) ∑_{k=0}^{n-1} k^p.

Русский

Альтернативная формула Фаульхера: B_{p+1}(n) = B_{p+1} + (p+1) ∑_{k=0}^{n-1} k^p.

LaTeX

$$bernoulli(p.succ).eval(n) = bernoulli(p.succ) + (p+1) ∑_{k=0}^{n-1} k^p$$

Lean4

/-- Rearrangement of `Polynomial.sum_range_pow_eq_bernoulli_sub`. -/
theorem bernoulli_succ_eval (n p : ℕ) :
    (bernoulli p.succ).eval (n : ℚ) = _root_.bernoulli p.succ + (p + 1 : ℚ) * ∑ k ∈ range n, (k : ℚ) ^ p :=
  by
  apply eq_add_of_sub_eq'
  rw [sum_range_pow_eq_bernoulli_sub]

Похожие утверждения