bernoulliFun_endpoints_eq_of_ne_one

English

Periodized Bernoulli is the Bernoulli polynomial lifted to the unit circle via the AddCircle construction.

Русский

Periodized Bernoulli — это Бернулли-полином, поднятый на единичную окружность через конструкцию AddCircle.

LaTeX

$$$$ \\text{periodizedBernoulli}(k) = \\text{liftIco}_{1,0}(\\bernoulliFun(k)). $$$$

Lean4

theorem bernoulliFun_endpoints_eq_of_ne_one {k : ℕ} (hk : k ≠ 1) : bernoulliFun k 1 = bernoulliFun k 0 := by
  rw [bernoulliFun_eval_zero, bernoulliFun, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one,
    bernoulli_eq_bernoulli'_of_ne_one hk, eq_ratCast]

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