English
The derivative of z^p(1 + ε(z)) is Θ(z^{p-1}) in the sense of asymptotic order, for any p ≠ 0.
Русский
Производная z^p(1 + ε(z)) имеет порядок роста Θ(z^{p-1}) при p ≠ 0.
LaTeX
$$$\\left|\\frac{d}{dz}\\bigl(z^p(1 + \\varepsilon(z))\\bigr)\\right| = Θ(z^{p-1}) \\quad (z \\to \\infty).$$$
Lean4
theorem growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) :
GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖ := by
cases eq_or_ne p 0 with
| inl hp => -- p = 0
have h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =ᶠ[atTop] fun z => z⁻¹ / (log z ^ 2) :=
by
filter_upwards [eventually_deriv_one_add_smoothingFn, eventually_gt_atTop 1] with x hx hx_pos
have : 0 ≤ x⁻¹ / (log x ^ 2) := by positivity
simp only [neg_div, norm_neg, hp, Real.rpow_zero, one_mul, hx, Real.norm_of_nonneg this]
refine GrowsPolynomially.congr_of_eventuallyEq h₁ ?_
refine
GrowsPolynomially.div (GrowsPolynomially.inv growsPolynomially_id)
(GrowsPolynomially.pow 2 growsPolynomially_log ?_)
filter_upwards [eventually_ge_atTop 1] with x hx using log_nonneg hx
| inr hp => -- p ≠ 0
refine
GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p - 1)) (isTheta_deriv_rpow_p_mul_one_add_smoothingFn hp) ?_
filter_upwards [eventually_gt_atTop 0] with _ _
positivity
