English
Let E be a normed space, f: E → R with a strict Fréchet derivative f' at x, and f(x) ≠ 0. Then the strict Fréchet derivative of y ↦ √(f(y)) at x is (1 / (2√(f(x)))) • f'.
Русский
Пусть E — нормированное пространство, f: E → R имеет строгую Фрéше-частичную производную f' в точке x и f(x) ≠ 0. Тогда строгая Фрéше-терминальная производная функции y ↦ √(f(y)) в точке x равна (1 / (2√(f(x)))) • f'.
LaTeX
$$$D\\!\\!\\mathrm{str}\\big(\\sqrt{f}\\big)(x) = \\left(\\frac{1}{2\\sqrt{f(x)}}\\right) \\cdot f'$$$
Lean4
theorem sqrt (hf : HasStrictFDerivAt f f' x) (hx : f x ≠ 0) :
HasStrictFDerivAt (fun y => √(f y)) ((1 / (2 * √(f x))) • f') x :=
(hasStrictDerivAt_sqrt hx).comp_hasStrictFDerivAt x hf
