cpow — Mathlib

English

If f,g are differentiable and f(x) lies in the slit plane, then the derivative of x ↦ f(x)^{g(x)} is given by the standard cpow formula.

Русский

Если f,g дифференцируемы и f(x) лежит в резке плоскости, производная x ↦ f(x)^{g(x)} задаётся стандартной формулой cpow.

LaTeX

$$$\\forall x, HasStrictFDerivAt (f^g) = (g f^{g-1}) f' + (f^g \\log f) g'$; ...$$$

Lean4

theorem cpow (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) (h0 : f x ∈ slitPlane) :
    HasStrictFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x :=
  (hasStrictFDerivAt_cpow (p := (f x, g x)) h0).comp x (hf.prodMk hg)

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