English
For any nonzero p, the derivative of z^p(1 + ε(z)) is asymptotically p z^{p−1} as z → ∞, matching the previous result in an equivalent sense.
Русский
Для любого p ≠ 0 производная z^p(1 + ε(z)) асимптотически равна p z^{p−1} при z → ∞ (эквивалентно предыдущему результату).
LaTeX
$$$\\displaystyle \\frac{d}{dz}\\bigl(z^p(1 + \\varepsilon(z))\\bigr) \\sim p\\,z^{p-1} \\quad (z \\to \\infty).$$$
Lean4
theorem isEquivalent_deriv_rpow_p_mul_one_sub_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_sub_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_sub_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 [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 _ _
