abs — Mathlib

English

If f is differentiable with derivative f' and f(x) ≠ 0, then the derivative of the absolute value is (sign f(x)) • f'.

Русский

Если f имеет строгую Фреше-производную f' в x и f(x) ≠ 0, то d|f|/dx в x равна sign(f(x))·f'.

LaTeX

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

Lean4

theorem abs (hf : HasStrictFDerivAt f f' x) (h₀ : f x ≠ 0) :
    HasStrictFDerivAt (fun x ↦ |f x|) ((SignType.sign (f x) : ℝ) • f') x :=
  by
  convert (hasStrictDerivAt_abs h₀).hasStrictFDerivAt.comp x hf using 1
  ext y
  simp [mul_comm]

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