const_cpow — Mathlib

English

If f,g have Frechet derivatives within a set s, then the map x ↦ f(x)^{g(x)} has a Frechet derivative within s with the expected cpow form.

Русский

Если f,g имеют производную внутри множества s, то f(x)^{g(x)} имеет производную внутри s по ожидаемой формуле cpow.

LaTeX

$$$\\\\forall f,g, HasFDerivWithinAt f f' s x, HasFDerivWithinAt g g' s x \\\\Rightarrow HasFDerivWithinAt (\\\\lambda x, f(x)^{g(x)}) s x$$$

Lean4

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

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