Derivative_of_Function_to_Power_of_Function
Proveddifferential-calculusexponential-functionproofwiki
Let be real functions which are differentiable on . Then
Preamble
import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Formal statement
theorem Derivative_of_Function_to_Power_of_Function (f g : ℝ → ℝ) (x : ℝ) (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (hfp : 0 < f x) : DifferentiableAt ℝ (fun x => (f x) ^ (g x)) x := by sorry
Source