abs — Mathlib

English

If f(x) ≠ 0, then the derivative of |f| is a scalar multiple of f' by sign(f(x)).

Русский

Если f(x) ≠ 0, то d|f|/dx = sign(f(x)) · f' в x.

LaTeX

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

Lean4

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

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