const_cpow — Mathlib

English

If f is differentiable at x and f(x) ∈ slitPlane, then the derivative of x ↦ c^{f(x)} is c^{f(x)} log c · f'(x).

Русский

Если f дифференцируема в x и f(x) ∈ slitPlane, то производная x ↦ c^{f(x)} равна c^{f(x)} log c · f'(x).

LaTeX

$$$\\text{If }f\\text{ is differentiable at }x\\text{ and }f(x)\\in\\mathrm{slitPlane},\\ \\frac{d}{dx} c^{f(x)} = c^{f(x)} \\log c \\cdot f'(x).$$$

Lean4

theorem const_cpow (hf : HasDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
    HasDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x :=
  (hasStrictDerivAt_const_cpow h0).hasDerivAt.comp x hf

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