const_rpow — Mathlib

English

If f has a Frechet derivative at x and c > 0, then the derivative of x ↦ c^{f(x)} at x is (c^{f(x)} log c) f'(x).

Русский

Если у f в точке x есть производная Фреше, то производная x ↦ c^{f(x)} в x равна c^{f(x)} log c · f'(x).

LaTeX

$$HasFDerivAt (fun x => c ^ f x) ((c ^ f x * log c) • f') x$$

Lean4

theorem const_rpow (hf : HasFDerivAt f f' x) (hc : 0 < c) :
    HasFDerivAt (fun x => c ^ f x) ((c ^ f x * Real.log c) • f') x :=
  (hasStrictDerivAt_const_rpow hc (f x)).hasDerivAt.comp_hasFDerivAt x hf

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