rpow — Mathlib

English

If x ≠ 0 or p ≥ 1, then the derivative of x^p is p x^{p-1}.

Русский

Если x ≠ 0 или p ≥ 1, производная x^p равна p x^{p-1}.

LaTeX

$$$\\forall x\\in\\mathbb{R},\\forall p\\in\\mathbb{R},\\ (x\\neq 0 \\lor p\\ge 1)\\Rightarrow \\dfrac{d}{dx} x^p = p x^{p-1}. $$$

Lean4

theorem rpow (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) (h : 0 < f x) :
    HasFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x := by
  exact (hasStrictFDerivAt_rpow_of_pos (f x, g x) h).hasFDerivAt.comp x (hf.prodMk hg)

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