antideriv_bernoulliFun — Mathlib

English

An antiderivative relation: the derivative of bernoulliFun at k+1 yields bernoulliFun(k).

Русский

Антипроизводная: производная bernoulliFun при k+1 даёт bernoulliFun(k).

LaTeX

$$$$ \\text{HasDerivAt}\\left( x \\mapsto \\frac{\\bernoulliFun(k+1)(x)}{k+1}, \\bernoulliFun(k)(x), x \\right). $$$$

Lean4

theorem antideriv_bernoulliFun (k : ℕ) (x : ℝ) :
    HasDerivAt (fun x => bernoulliFun (k + 1) x / (k + 1)) (bernoulliFun k x) x :=
  by
  convert (hasDerivAt_bernoulliFun (k + 1) x).div_const _ using 1
  simp [Nat.cast_add_one_ne_zero k]

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