abs_of_pos — Mathlib

English

If f is differentiable with strict derivative f' at x and f(x) > 0, then the derivative of |f| is f' at x.

Русский

Если f обладает строгой Фреше-производной f' в x и f(x) > 0, то d|f|/dx|_x = f'(x).

LaTeX

$$HasStrictFDerivAt f f' x ∧ 0 < f x ⇒ HasStrictFDerivAt ($ \lambda x, |f x| $) f' x$$

Lean4

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

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