periodizedBernoulli — Mathlib

English

Definition of periodizedBernoulli as lifting BernoulliFun to the unit circle.

Русский

Определение periodizedBernoulli как отображение БернуллиFun на единичную окружность через подъем.

LaTeX

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

Lean4

/-- The Bernoulli polynomial, extended from `[0, 1)` to the unit circle. -/
def periodizedBernoulli (k : ℕ) : 𝕌 → ℝ :=
  AddCircle.liftIco 1 0 (bernoulliFun k)

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