English
The derivative of z^p(1 − ε(z)) grows polynomially with exponent p−1; more precisely, if p ≠ 0, then the derivative grows like z^{p−1} up to multiplicative constants.
Русский
Производная z^p(1 − ε(z)) растет как степенная функция с экспонентой p−1; если p ≠ 0, она растет как z^{p−1} до констант.
LaTeX
$$$\\text{If } p \\neq 0,\\quad \\mathrm{d}(z^p(1 - \\varepsilon(z))) = \\Theta(z^{p-1}).$$$
Lean4
theorem growsPolynomially_deriv_rpow_p_mul_one_sub_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_sub_smoothingFn, eventually_gt_atTop 1] with x hx hx_pos
have : 0 ≤ x⁻¹ / (log x ^ 2) := by positivity
simp only [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 _ hx using log_nonneg hx
| inr hp => -- p ≠ 0
refine
GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p - 1)) (isTheta_deriv_rpow_p_mul_one_sub_smoothingFn hp) ?_
filter_upwards [eventually_gt_atTop 0] with _ _
positivity
