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]