logDeriv_eq_zero_of_not_differentiableAt

English

If a function f is not differentiable at x, then the logarithmic derivative logDeriv f x equals 0.

Русский

Если функция f не дифференцируема в точке x, то логарифмическая производная logDeriv f x равна 0.

LaTeX

$$$\lnot \text{DifferentiableAt}_{\mathbb{K}}(f,x) \Rightarrow \logDeriv f x = 0$$$

Lean4

theorem logDeriv_eq_zero_of_not_differentiableAt (f : 𝕜 → 𝕜') (x : 𝕜) (h : ¬DifferentiableAt 𝕜 f x) :
    logDeriv f x = 0 := by simp only [logDeriv_apply, deriv_zero_of_not_differentiableAt h, zero_div]

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