English
If a < 0, the map x ↦ a^x is strictly differentiable with derivative a^x log a − exp(log a · x) sin(xπ) π.
Русский
Если a < 0, функция x ↦ a^x строго дифференцируема; производная равна a^x log a − exp(log a · x) sin(xπ) π.
LaTeX
$$$\\text{If } a<0:\\\\ \\frac{d}{dx} a^x = a^x \\log a - \\exp(\\log a \\cdot x) \\sin(x\\pi) \\pi.$$$
Lean4
/-- This lemma says that `fun x => a ^ x` is strictly differentiable for `a < 0`. Note that these
values of `a` are outside of the "official" domain of `a ^ x`, and we may redefine `a ^ x`
for negative `a` if some other definition will be more convenient. -/
theorem hasStrictDerivAt_const_rpow_of_neg {a x : ℝ} (ha : a < 0) :
HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a - exp (log a * x) * sin (x * π) * π) x := by
simpa using
(hasStrictFDerivAt_rpow_of_neg (a, x) ha).comp_hasStrictDerivAt x
((hasStrictDerivAt_const _ _).prodMk (hasStrictDerivAt_id _))
