English
A refined real-analytic formation shows that, away from zero, the map y ↦ y^{r} has a derivative given by r y^{r-1} and the complex-pow identities carry through with appropriate branch choices.
Русский
Уточненная вещественно-аналитическая формула показывает, что вне нуля отображение y ↦ y^{r} имеет производную r y^{r-1} и соответствуют свойства комплексной степени с корректными выборками ветви.
LaTeX
$$$\\text{For }y\\neq 0\\text{ and }r\\in\\mathbb{C},\\ \\frac{d}{dy} (y^{r}) = r y^{r-1}$ (with appropriate branch considerations).$$$
Lean4
/-- An alternate formulation of `hasDerivAt_ofReal_cpow_const'`. -/
theorem hasDerivAt_ofReal_cpow_const {x : ℝ} (hx : x ≠ 0) {r : ℂ} (hr : r ≠ 0) :
HasDerivAt (fun y : ℝ => (y : ℂ) ^ r) (r * x ^ (r - 1)) x :=
by
have := HasDerivAt.const_mul r <| hasDerivAt_ofReal_cpow_const' hx (by rwa [ne_eq, sub_eq_neg_self])
simpa [sub_add_cancel, mul_div_cancel₀ _ hr] using this
