const_cpow — Mathlib

English

If f: domain → ℂ is differentiable and f(x) ∈ slitPlane for all x, then the derivative of x ↦ c^{f(x)} is c^{f(x)} log c · f'(x) at every x.

Русский

Если f: домен → ℂ дифференцируема и для всех x выполняется f(x) ∈ slitPlane, то производная x ↦ c^{f(x)} равна c^{f(x)} log c · f'(x) на каждой точке.

LaTeX

$$$\\text{Let }f\\text{ be differentiable on the domain and }f(x)\\in\\mathrm{slitPlane}\\text{ for all }x.\\quad \\frac{d}{dx} \\bigl(c^{f(x)}\\bigr)= c^{f(x)} \\log c \\ f'(x).$$$

Lean4

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

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