rpow — Mathlib

English

If f and g have derivatives at x and f(x) > 0, then the derivative of f(x)^{g(x)} is given by the usual product rule with log f.

Русский

Если в точке x конечны производные f и g и f(x) > 0, то производная f(x)^{g(x)} описывается правилом произведения с log f.

LaTeX

$$HasDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x$$

Lean4

theorem rpow (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) (h : 0 < f x) :
    HasDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x :=
  by
  rw [← hasDerivWithinAt_univ] at *
  exact hf.rpow hg h

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