arctan — Mathlib

English

If f has a strict derivative, then arctan ∘ f has a strict derivative with factor (1/(1+(f x)^2)).

Русский

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

LaTeX

$$$ \text{Theorem: } \text{HasStrictDerivAt arctan}( f(x) ) \Rightarrow \text{HasStrictDerivAt } (x \mapsto \arctan(f(x))) \left( \frac{1}{1+(f(x))^2} f' \right). $$$

Lean4

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

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