hasStrictDerivAt_log_of_pos — Mathlib

English

For x > 0, log has derivative 1/x at x; i.e., the derivative of log at a positive point is x⁻¹.

Русский

При x > 0 производная логарифма есть 1/x; то есть производная log в положительной точке равна x⁻¹.

LaTeX

$$$$ \\frac{d}{dx}\\log x = \\frac{1}{x} \\quad (x>0). $$$$

Lean4

theorem hasStrictDerivAt_log_of_pos (hx : 0 < x) : HasStrictDerivAt log x⁻¹ x :=
  by
  have : HasStrictDerivAt log (exp <| log x)⁻¹ x :=
    (hasStrictDerivAt_exp <| log x).of_local_left_inverse (continuousAt_log hx.ne') (ne_of_gt <| exp_pos _) <|
      Eventually.mono (lt_mem_nhds hx) @exp_log
  rwa [exp_log hx] at this

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