bernoulli_def — Mathlib

English

The Bernoulli polynomial B_n is given by a sum over i from 0 to n, with terms involving Bernoulli numbers and binomial coefficients.

Русский

Полином Бернулли B_n выражается суммой по i от 0 до n, с участием чисел Бернулли и биномиальных коэффициентов.

LaTeX

$$bernoulli(n) = ∑_{i=0}^{n} binom(n,i) bernoulli(n-i) ⋅ X^{i}$$

Lean4

theorem bernoulli_def (n : ℕ) :
    bernoulli n = ∑ i ∈ range (n + 1), Polynomial.monomial i (_root_.bernoulli (n - i) * choose n i) :=
  by
  rw [← sum_range_reflect, add_succ_sub_one, add_zero, bernoulli]
  apply sum_congr rfl
  rintro x hx
  rw [mem_range_succ_iff] at hx
  rw [choose_symm hx, tsub_tsub_cancel_of_le hx]
    /-
    ### examples
    -/

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