rightDeriv_klFun — Mathlib

English

The right 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 right 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 rightDeriv_klFun : derivWithin klFun (Ioi x) x = log x :=
  by
  by_cases h0 : x = 0
  · simp only [h0, log_zero]
    exact derivWithin_zero_of_not_differentiableWithinAt not_differentiableWithinAt_klFun_Ioi_zero
  · exact (hasDerivAt_klFun h0).hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Ioi x)

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