const_cpow — Mathlib

English

If f has strict derivative and c ≠ 0 or f(x) ≠ 0, then the map x ↦ c^{f(x)} is strictly differentiable with derivative (c^{f(x)} log c) f'.

Русский

Если f имеет строгую производную и c ≠ 0 или f(x) ≠ 0, то x ↦ c^{f(x)} дифференцируемо с производной (c^{f(x)} log c) f'.

LaTeX

$$$\\\\forall f',x,c, HasStrictFDerivAt f f' x \\Rightarrow \\; HasStrictFDerivAt (\\\\lambda x, c^{f(x)}) ((c^{f(x)} \\log c) f') x$$$

Lean4

theorem const_cpow (hf : HasStrictFDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
    HasStrictFDerivAt (fun x => c ^ f x) ((c ^ f x * Complex.log c) • f') x :=
  (hasStrictDerivAt_const_cpow h0).comp_hasStrictFDerivAt x hf

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