sqrt — Mathlib

English

Let E be a normed space, f: E → R, differentiable at x with derivative f' (a linear map). If f(x) ≠ 0, then the Fréchet derivative of y ↦ √(f(y)) at x is (1 / (2√(f(x)))) • f'.

Русский

Пусть E — нормированное пространство, f: E → R дифференцируема в точке x с производной f'. Если f(x) ≠ 0, то Фрéше-дифференциал функции y ↦ √(f(y)) в точке x равен (1 / (2√(f(x)))) • f'.

LaTeX

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

Lean4

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

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