hasDerivAt_klFun — Mathlib

English

For every x ≠ 0, the derivative of klFun at x is log x.

Русский

Для каждого x ≠ 0 производная klFun в точке x равна log x.

LaTeX

$$$\\frac{d}{dx}\\mathrm{klFun}(x) = \\log x \\quad \\text{for } x \\neq 0$$$

Lean4

/-- The derivative of `klFun` at `x ≠ 0` is `log x`. -/
theorem hasDerivAt_klFun (hx : x ≠ 0) : HasDerivAt klFun (log x) x :=
  by
  convert ((hasDerivAt_mul_log hx).add (hasDerivAt_const x 1)).sub (hasDerivAt_id x) using 1
  ring

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