English
Let p be a real number. The derivative of the function z ↦ z^p(1 − ε(z)) satisfies, for large z, an asymptotic expansion: d/dz[z^p(1 − ε(z))] ~ p z^{p−1}(1 − ε(z)) + z^{p−1}/(log z)^2.
Русский
Пусть p — произвольное действительное число. Производная по z функции z ↦ z^p(1 − ε(z)) имеет асимптотическое разложение при больших z: d/dz[z^p(1 − ε(z))] ~ p z^{p−1}(1 − ε(z)) + z^{p−1}/(log z)^2.
LaTeX
$$$\\displaystyle \\frac{d}{dz}\\bigl(z^p\\,(1 - \\varepsilon(z))\\bigr) \\sim p\\,z^{p-1}\\,(1 - \\varepsilon(z)) \\;+\\; \\frac{z^{p-1}}{(\\log z)^2} \\quad \\text{as } z \\to \\infty.$$$
Lean4
theorem eventually_deriv_rpow_p_mul_one_sub_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 z => z ^ p * (1 - ε z))
_ =ᶠ[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_sub_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_sub_smoothingFn] with x hx hderiv
rw [hderiv, Real.deriv_rpow_const (Or.inl <| by positivity)]
_ =ᶠ[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
rw [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]
