bernoulliFun_eval_one — Mathlib

English

A technical, auxiliary fact about the periodized Bernoulli function used in the subsequent arguments (supporting Gallagher-type results).

Русский

Техническое вспомогательное свойство periodizedBernoulli, используемое далее в доказательствах типа Галлахера.

LaTeX

$$$$ \\text{(auxiliary property of periodizedBernoulli).} $$$$

Lean4

theorem bernoulliFun_eval_one (k : ℕ) : bernoulliFun k 1 = bernoulliFun k 0 + ite (k = 1) 1 0 :=
  by
  rw [bernoulliFun, bernoulliFun_eval_zero, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one]
  split_ifs with h
  · rw [h, bernoulli_one, bernoulli'_one, eq_ratCast]
    push_cast; ring
  · rw [bernoulli_eq_bernoulli'_of_ne_one h, add_zero, eq_ratCast]

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