abs_of_neg — Mathlib

English

If f(x) ≠ 0, then HasStrictFDerivAt (abs ∘ f) equals a suitable scalar multiple of f′.

Русский

Если f(x) ≠ 0, то производная |f| совпадает с допустимым скалярным умножением на производную f′.

LaTeX

$$HasStrictFDerivAt f f' x ∧ f x ≠ 0 ⇒ HasStrictFDerivAt (abs ∘ f) ((SignType.sign (f x)) • f') x$$

Lean4

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

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