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)