leftDeriv_klFun — Mathlib

English

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

Русский

Левый предел производной klFun равен log x, т.е. производная слева klFun(x) = log x.

LaTeX

$$$\\dfrac{d}{dx^-}\\mathrm{klFun}(x) = \\log x$$$

Lean4

/-- The left derivative of `klFun` is `log x`. This also holds at `x = 0` although `klFun` is not
differentiable there since the default value of `derivWithin` in that case is 0. -/
@[simp]
theorem leftDeriv_klFun : derivWithin klFun (Iio x) x = log x :=
  by
  by_cases h0 : x = 0
  · simp only [h0, log_zero]
    exact derivWithin_zero_of_not_differentiableWithinAt not_differentiableWithinAt_klFun_Iio_zero
  · exact (hasDerivAt_klFun h0).hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Iio x)

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