bernoulli_eval_one — Mathlib

English

Translation formula for Bernoulli polynomials: B_n(1+x) = B_n(x) + n x^{n-1}.

Русский

Формула переноса для Бернулли-полиномов: B_n(1+x) = B_n(x) + n x^{n-1}.

LaTeX

$$$\text{bernoulliEvalOneAdd}(n) : B_n(1+x) = B_n(x) + n x^{n-1}$$$

Lean4

@[simp]
theorem bernoulli_eval_one (n : ℕ) : (bernoulli n).eval 1 = bernoulli' n :=
  by
  simp only [bernoulli, eval_finset_sum]
  simp only [← succ_eq_add_one, sum_range_succ, mul_one, cast_one, choose_self, (_root_.bernoulli _).mul_comm,
    sum_bernoulli, one_pow, mul_one, eval_monomial, one_mul]
  by_cases h : n = 1
  · norm_num [h]
  · simp [h, bernoulli_eq_bernoulli'_of_ne_one h]

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