fderiv_arctan — Mathlib

English

If f is differentiable at x, then the derivative of arctan(f(x)) at x is (1 / (1 + f(x)^2)) times the derivative of f at x.

Русский

Если f дифференцируема в x, то производная arctan(f(x)) по x равна (1 / (1 + f(x)^2)) умножить на производную f в x.

LaTeX

$$$fderiv_\mathbb{R}(\arctan \circ f)(x) = \dfrac{1}{1 + f(x)^2} \; fderiv_\mathbb{R} f(x).$$$

Lean4

@[simp]
theorem fderiv_arctan (hc : DifferentiableAt ℝ f x) :
    fderiv ℝ (fun x => arctan (f x)) x = (1 / (1 + f x ^ 2)) • fderiv ℝ f x :=
  hc.hasFDerivAt.arctan.fderiv

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