deriv_sqrt — Mathlib

English

Let f: R → R be differentiable at x with f(x) ≠ 0. Then the derivative of the function x ↦ √(f(x)) at x is given by (f'(x)) / (2√(f(x))). Equivalently, d/dx √(f(x)) = f'(x) / (2√(f(x))).

Русский

Пусть f: R → R дифференцируема в точке x и f(x) ≠ 0. Тогда производная функции x ↦ √(f(x)) в точке x равна f'(x) / (2√(f(x))).

LaTeX

$$$\\frac{d}{dx}\\sqrt{f(x)} = \\frac{f'(x)}{2\\sqrt{f(x)}}$$$

Lean4

@[simp]
theorem deriv_sqrt (hf : DifferentiableAt ℝ f x) (hx : f x ≠ 0) :
    deriv (fun x => √(f x)) x = deriv f x / (2 * √(f x)) :=
  (hf.hasDerivAt.sqrt hx).deriv

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