const_rpow — Mathlib

English

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

Русский

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

LaTeX

$$HasStrictFDerivAt (fun x => c ^ f x) ((c ^ f x * Real.log c) • f') x$$

Lean4

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

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