Theorems · Theorem · real analysis

HasDerivWithinAt.rpow

∀ {f g : ℝ → ℝ} {f' g' x : ℝ} {s : Set ℝ},
  HasDerivWithinAt f f' s x →
    HasDerivWithinAt g g' s x →
      0 < f x → HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x

Defined in

Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Cited by

2 results in Mathlib

Foundations

Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound