English
The norm of the derivative of z^p(1 + ε(z)) grows like z^{p−1}; more precisely, the L2 norm of the derivative is Θ(z^{p−1}).
Русский
Нормa производной функции z^p(1 + ε(z)) растет как z^{p−1}; точнее, нормa L2 производной равна Θ(z^{p−1}).
LaTeX
$$$\\|\\mathrm{d}(z^p(1 + \\varepsilon(z)))/\\mathrm{d}z\\| = Θ(z^{p-1})$ as $z \\to \\infty$.$$
Lean4
theorem isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn {p : ℝ} (hp : p ≠ 0) :
deriv (fun z => z ^ p * (1 + ε z)) ~[atTop] fun z => p * z ^ (p - 1) :=
calc
deriv (fun z => z ^ p * (1 + ε z))
_ =ᶠ[atTop] fun z => p * z ^ (p - 1) * (1 + ε z) - z ^ (p - 1) / (log z ^ 2) :=
(eventually_deriv_rpow_p_mul_one_add_smoothingFn p)
_ ~[atTop] fun z => p * z ^ (p - 1) :=
by
refine IsEquivalent.add_isLittleO ?one ?two
case one =>
calc
(fun z => p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p - 1) * 1 :=
IsEquivalent.mul IsEquivalent.refl isEquivalent_one_add_smoothingFn_one
_ = fun z => p * z ^ (p - 1) := by ext; ring
case two =>
calc
(fun z => -(z ^ (p - 1) / (log z ^ 2))) =o[atTop] fun z => z ^ (p - 1) / 1 :=
by
simp_rw [isLittleO_neg_left, div_eq_mul_inv]
refine IsBigO.mul_isLittleO (isBigO_refl _ _) (IsLittleO.inv_rev ?_ (by simp))
rw [isLittleO_const_left]
refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
exact Tendsto.comp (g := fun z => z ^ 2) (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
_ = fun z => z ^ (p - 1) := by ext; simp
_ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _
