Theorems · Theorem · real analysis

HasFDerivWithinAt.cpow

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ} {f' g' : StrongDual ℂ E} {x : E}
  {s : Set E},
  HasFDerivWithinAt f f' s x →
    HasFDerivWithinAt g g' s x →
      f x ∈ Complex.slitPlane →
        HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x

Defined in

Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace