English
If f,g: E → ℝ are differentiable within s at x, and f(x) > 0, then the map x ↦ f(x)^{g(x)} has a Fréchet derivative within s at x given by the linear combination of f' and g' with coefficients g(x) f(x)^{g(x)-1} and f(x)^{g(x)} log f(x).
Русский
Пусть f,g: E → ℝ дифференцируемы внутри s в x, и f(x) > 0; тогда x ↦ f(x)^{g(x)} имеет Ферме-дифференциал внутри s в x с линейной комбинацией коэффициентов.
LaTeX
$$$\\text{If } hf:HasFDerivWithinAt f f' s x,\\; hg:HasFDerivWithinAt g g' s x,\\; h: f x>0, \\\\ HasFDerivWithinAt (f^g)\\; s\\; x = (g x f x^{g x-1}) f' + (f x^{g x} \\log(f x))\\, g'.$$$
Lean4
theorem rpow (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) (h : 0 < f x) :
HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') s x := by
-- `by exact` to deal with tricky unification.
exact (hasStrictFDerivAt_rpow_of_pos (f x, g x) h).hasFDerivAt.comp_hasFDerivWithinAt x (hf.prodMk hg)
