deriv_klFun — Mathlib

English

The derivative of klFun is log, i.e., d/dx klFun(x) = log x.

Русский

Производная klFun равна log x, то есть d/dx klFun(x) = log x.

LaTeX

$$$\\frac{d}{dx}\\mathrm{klFun}(x) = \\log x$$$

Lean4

/-- The derivative of `klFun` is `log x`. This also holds at `x = 0` although `klFun` is not
differentiable there since the default value of `deriv` in that case is 0. -/
@[simp]
theorem deriv_klFun : deriv klFun = log := by
  ext x
  by_cases h0 : x = 0
  · simp only [h0, log_zero]
    exact deriv_zero_of_not_differentiableAt not_differentiableAt_klFun_zero
  · exact (hasDerivAt_klFun h0).deriv

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