deriv_log — Mathlib

English

The derivative of log at x is 1/x for x ≠ 0; at x = 0 it is conventionally defined as 0 in this formal setting.

Русский

Производная логарифма в точке x равна 1/x при x ≠ 0; в точке x = 0 производная при данной формализации равна 0.

LaTeX

$$$\\frac{d}{dx}\\log x = x^{-1} \\quad (x \\neq 0);\\; \\frac{d}{dx}\\log x|_{x=0} = 0$$$

Lean4

theorem deriv_log (x : ℝ) : deriv log x = x⁻¹ :=
  if hx : x = 0 then by rw [deriv_zero_of_not_differentiableAt (differentiableAt_log_iff.not_left.2 hx), hx, inv_zero]
  else (hasDerivAt_log hx).deriv

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