arctan

Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

URI: https://scilib.ai/kg/mathlib#HasDerivAt.arctan

English

If f has derivative f' at x, then arctan ∘ f has derivative (1/(1+f(x)^2))·f'(x) at x.

Русский

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

LaTeX

$$$ \text{HasDerivAt arctan }(f(x)) \ (1/(1+f(x)^2)) \cdot f' $$$

Lean4

theorem arctan (hf : HasDerivAt f f' x) : HasDerivAt (fun x => arctan (f x)) (1 / (1 + f x ^ 2) * f') x :=
  (Real.hasDerivAt_arctan (f x)).comp x hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru