English
The derivative of the real-valued function x ↦ x^{c} (viewed in ℂ) has Theta-equivalence with x^{c.re-1} as x → ∞, i.e., is Theta of x^{c.re-1} at infinity.
Русский
Производная функции x ↦ x^{c} (как комплексная) эквивалентна по теории Θ выражению x^{c.re-1} на бесконечности.
LaTeX
$$$\\text{If }c\\in\\mathbb{C},\\ c\\neq 0:\\ \\mathrm{deriv}\\bigl(x\\mapsto x^{c}\\bigr)=\\Theta_{x\\to\\infty} x^{c_{\\mathrm{re}}-1}.$$$
Lean4
theorem isTheta_deriv_ofReal_cpow_const_atTop {c : ℂ} (hc : c ≠ 0) :
deriv (fun (x : ℝ) => (x : ℂ) ^ c) =Θ[atTop] fun x => x ^ (c.re - 1) := by
calc
_ =ᶠ[atTop] fun x : ℝ ↦ c * x ^ (c - 1) := by
filter_upwards [eventually_ne_atTop 0] with x hx using by rw [deriv_ofReal_cpow_const hx hc]
_ =Θ[atTop] fun x : ℝ ↦ ‖(x : ℂ) ^ (c - 1)‖ :=
((Asymptotics.IsTheta.of_norm_eventuallyEq EventuallyEq.rfl).const_mul_left hc)
_ =ᶠ[atTop] fun x ↦ x ^ (c.re - 1) :=
by
filter_upwards [eventually_gt_atTop 0] with x hx
rw [norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]
