hasDerivAt_bernoulliFun — Mathlib

English

The derivative of bernoulliFun with respect to x satisfies HasDerivAt(bernoulliFun k, k·bernoulliFun(k−1) x, x).

Русский

Производная bernoulliFun по x равна k·bernoulliFun(k−1)(x).

LaTeX

$$$$ \\text{HasDerivAt}(\\bernoulliFun(k), k \\cdot \\bernoulliFun(k-1)(x), x). $$$$

Lean4

theorem hasDerivAt_bernoulliFun (k : ℕ) (x : ℝ) : HasDerivAt (bernoulliFun k) (k * bernoulliFun (k - 1) x) x :=
  by
  convert ((Polynomial.bernoulli k).map <| algebraMap ℚ ℝ).hasDerivAt x using 1
  simp only [bernoulliFun, Polynomial.derivative_map, Polynomial.derivative_bernoulli k, Polynomial.map_mul,
    Polynomial.map_natCast, Polynomial.eval_mul, Polynomial.eval_natCast]

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