bernoulli_three_eval_one_quarter — Mathlib

English

The third Bernoulli polynomial evaluates at 1/4 to 3/64: B3(1/4) = 3/64.

Русский

Третий Бернулли-полином в точке 1/4 дает 3/64: B3(1/4) = 3/64.

LaTeX

$$$(\text{Polynomial.bernoulli } 3).\text{eval}(\tfrac{1}{4}) = \tfrac{3}{64}.$$$

Lean4

theorem bernoulli_three_eval_one_quarter : (Polynomial.bernoulli 3).eval (1 / 4) = 3 / 64 :=
  by
  simp_rw [Polynomial.bernoulli, Finset.sum_range_succ, Polynomial.eval_add, Polynomial.eval_monomial]
  rw [Finset.sum_range_zero, Polynomial.eval_zero, zero_add, bernoulli_one]
  rw [bernoulli_eq_bernoulli'_of_ne_one zero_ne_one, bernoulli'_zero,
    bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1), bernoulli'_two,
    bernoulli_eq_bernoulli'_of_ne_one (by decide : 3 ≠ 1), bernoulli'_three]
  norm_num

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