fderiv_sqrt — Mathlib

English

If f is differentiable at x and f(x) ≠ 0, then the derivative in the sense of fderiv at x of y ↦ √(f(y)) equals (1/(2√(f(x)))) • fderiv f x.

Русский

Если f дифференцируема в точке x и f(x) ≠ 0, то fderiv в точке x от y ↦ √(f(y)) равен (1/(2√(f(x)))) • fderiv f x.

LaTeX

$$$fderiv\\_\\mathbb{R}\\,(\\sqrt{f})\\, x = \\left(\\frac{1}{2\\sqrt{f(x)}}\\right) \\cdot fderiv\\_\\mathbb{R} f\\, x$$$

Lean4

@[simp]
theorem fderiv_sqrt (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) :
    fderiv ℝ (fun x => √(f x)) x = (1 / (2 * √(f x))) • fderiv ℝ f x :=
  (hf.hasFDerivAt.sqrt hx).fderiv

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