English
If hp is nonzero, the derivative of z^p(1 + ε(z)) is asymptotically equivalent to p z^{p−1} as z grows: d/dz[z^p(1 + ε(z))] ~ p z^{p−1}.
Русский
Если hp ≠ 0, производная функции z^p(1 + ε(z)) асимптотически эквивалентна p z^{p−1} при больших z: d/dz[z^p(1 + ε(z))] ~ p z^{p−1}.
LaTeX
$$$\\displaystyle \\frac{d}{dz}\\bigl(z^p(1 + \\varepsilon(z))\\bigr) \\sim p\\,z^{p-1} \\quad (z \\to \\infty).$$$
Lean4
theorem eventually_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) :
deriv (fun z => z ^ p * (1 + ε z)) =ᶠ[atTop] fun z => p * z ^ (p - 1) * (1 + ε z) - z ^ (p - 1) / (log z ^ 2) :=
calc
deriv (fun x => x ^ p * (1 + ε x))
_ =ᶠ[atTop] fun x => deriv (· ^ p) x * (1 + ε x) + x ^ p * deriv (1 + ε ·) x :=
by
filter_upwards [eventually_gt_atTop 1] with x hx
rw [deriv_fun_mul]
· exact differentiableAt_rpow_const_of_ne _ (by positivity)
· exact differentiableAt_one_add_smoothingFn hx
_ =ᶠ[atTop] fun x => p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / (log x ^ 2)) :=
by
filter_upwards [eventually_gt_atTop 1, eventually_deriv_one_add_smoothingFn] with x hx hderiv
simp [hderiv, Real.deriv_rpow_const (Or.inl <| by positivity), neg_div, sub_eq_add_neg]
_ =ᶠ[atTop] fun x => p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / (log x ^ 2) :=
by
filter_upwards [eventually_gt_atTop 0] with x hx
simp [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]
