arctan — Mathlib

English

Let E be a normed space and f: E → ℝ differentiable at x with Fréchet derivative f'. Then the derivative of arctan(f(x)) at x is (1 / (1 + f(x)^2)) • f'.

Русский

Пусть E — нормированное пространство, f: E → ℝ дифференцируема в точке x с производной f'. Тогда производная arctan(f(x)) по x равна (1 / (1 + f(x)^2)) • f'.

LaTeX

$$$D\,\big(\arctan \circ f\big)(x) = \dfrac{1}{1 + f(x)^2} \; Df(x).$$$

Lean4

theorem arctan (hf : HasFDerivAt f f' x) : HasFDerivAt (fun x => arctan (f x)) ((1 / (1 + f x ^ 2)) • f') x :=
  (hasDerivAt_arctan (f x)).comp_hasFDerivAt x hf

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