arsinh — Mathlib

English

If f has a strict Fréchet derivative f' at a, then arsinh ∘ f has the derivative ((√(1+f(a)^2))^{-1}) • f' at a.

Русский

Если f имеет строгий Фрéше производную f' в точке a, то arsinh(f) имеет производную ( (√(1+f(a)^2))^{-1} ) • f' в точке a.

LaTeX

$$$\\forall E\\ {\\text{Type }},\\ {f:X\\to\\mathbb{R}},\\ {a:E},\\ {f':\\text{StrongDual }\\mathbb{R} E},\\ HasStrictFDerivAt f f' a \\Rightarrow HasStrictFDerivAt (\\lambda x. \\operatorname{arsinh}(f x)) ( (\\sqrt{1 + f(a)^2})^{-1} \\cdot f') a.$$$

Lean4

theorem arsinh (hf : HasStrictFDerivAt f f' a) :
    HasStrictFDerivAt (fun x => arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a :=
  (hasStrictDerivAt_arsinh _).comp_hasStrictFDerivAt a hf

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