const_rpow — Mathlib

English

If f has a Frechet derivative within s at x, and c > 0, then f ↦ c^{f} has derivative within s at x given by the product rule with log c.

Русский

Если у f есть Фрешевая производная внутри области, и c>0, то производная функции x ↦ c^{f(x)} внутри области равна произведению логарифма c и производной f.

LaTeX

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

Lean4

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

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