arsinh — Mathlib

English

If f has Fréchet derivative f' within a set s at a, then arsinh ∘ f has Fréchet derivative within s at a with multiplier ((√(1+f(a)^2))^{-1}) • f'.

Русский

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

LaTeX

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

Lean4

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

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