arsinh — Mathlib

English

If f: E → ℝ is Fréchet differentiable at a with derivative f', then arsinh ∘ f is Fréchet differentiable at a with derivative ((√(1+f(a)^2))^{-1}) • f'.

Русский

Пусть f: E → ℝ имеет в точке a гладкую Фреше-дифференцируемость с производной f'. Тогда arsinh ∘ f гладка в точке a, и её производная равна ((√(1+f(a)^2))^{-1}) • f'.

LaTeX

$$$\text{HasFDerivAt } f\ f'\ a \;\Rightarrow\; \text{HasFDerivAt } (x \mapsto \operatorname{arsinh}(f(x)))\ \big( (\sqrt{1 + f(a)^2})^{-1} \cdot f' \big)\ a$$$

Lean4

theorem arsinh (hf : HasFDerivAt f f' a) : HasFDerivAt (fun x => arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a :=
  (hasDerivAt_arsinh _).comp_hasFDerivAt a hf

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