sqrt — Mathlib

English

If f has a Fréchet derivative f' within a set s at x and f(x) ≠ 0, then the function y ↦ √(f(y)) has Fréchet derivative within s at x, equal to (1 / (2√(f(x)))) • f'.

Русский

Если в точке x на области s функция f имеет производную Фрéше внутри s, и f(x) ≠ 0, то функция y ↦ √(f(y)) имеет внутри s производную Фрéше в точке x, равную (1 / (2√(f(x)))) • f'.

LaTeX

$$$D\\!\\!_s(\\sqrt{f})(x) = \\left(\\frac{1}{2\\sqrt{f(x)}}\\right) \\cdot f'$$$

Lean4

theorem sqrt (hf : HasFDerivWithinAt f f' s x) (hx : f x ≠ 0) :
    HasFDerivWithinAt (fun y => √(f y)) ((1 / (2 * √(f x))) • f') s x :=
  (hasDerivAt_sqrt hx).comp_hasFDerivWithinAt x hf

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