abs_of_pos — Mathlib

English

Let f be differentiable within s at x with derivative f'. If f(x) > 0, then the derivative of |f| at x within s is f'.

Русский

Пусть f дифференцируема внутри множества s в x с производной f'. Если f(x) > 0, то производная |f| в x внутри s равна f'.

LaTeX

$$$\operatorname{HasFDerivWithinAt} f f' s x \Rightarrow 0 < f(x) \Rightarrow \operatorname{HasFDerivWithinAt} (\lambda y, |f(y)|) f' \, s \ x$$$

Lean4

theorem abs_of_pos (hf : HasFDerivWithinAt f f' s x) (h₀ : 0 < f x) : HasFDerivWithinAt (fun x ↦ |f x|) f' s x :=
  by
  convert (hasDerivAt_abs_pos h₀).comp_hasFDerivWithinAt x hf using 1
  simp

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