bernoulliFun — Mathlib

English

Bernoulli function B_k is defined as the real-valued evaluation of the rational Bernoulli polynomial B_k via the Bernoulli numbers.

Русский

Бернулли-функция B_k есть реальное значение bernoulli-полинома B_k, полученное из рациональных коэффициентов Бернулли через отображение в ℝ и последующее вычисление в x.

LaTeX

$$$$ B_k(x) = (\\text{Bernoulli polynomial of degree } k)\\big|_{\\mathbb{Q} \\to \\mathbb{R}} (x). $$$$

Lean4

/-- The function `x ↦ Bₖ(x) : ℝ → ℝ`. -/
def bernoulliFun (k : ℕ) (x : ℝ) : ℝ :=
  (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)).eval x

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