abs_of_neg — Mathlib

English

If f is differentiable in the Fréchet sense at x with derivative f', and f(x) ≠ 0, then the derivative of the absolute value is (sign f(x)) · f'.

Русский

Если f имеет производную Фреше в точке x и f(x) ≠ 0, то производная |f| в x равна (sign f(x)) · f'.

LaTeX

$$HasFDerivAt f f' x ∧ f x ≠ 0 ⇒ HasFDerivAt ($ \lambda x, |f x| $) ((SignType.sign (f x)) • f') x$$

Lean4

theorem abs_of_neg (hf : HasFDerivAt f f' x) (h₀ : f x < 0) : HasFDerivAt (fun x ↦ |f x|) (-f') x :=
  by
  convert (hasDerivAt_abs_neg h₀).hasFDerivAt.comp x hf using 1
  ext y
  simp

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