isTheta_deriv_rpow_p_mul_one_sub_smoothingFn

English

For hp ≠ 0, the derivative of z^p(1 + ε(z)) is asymptotically p z^{p−1}; in other words, deriv(...) ~ p z^{p−1} as z → ∞.

Русский

При hp ≠ 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 isTheta_deriv_rpow_p_mul_one_sub_smoothingFn {p : ℝ} (hp : p ≠ 0) :
    (fun x => ‖deriv (fun z => z ^ p * (1 - ε z)) x‖) =Θ[atTop] fun z => z ^ (p - 1) :=
  by
  refine IsTheta.norm_left ?_
  calc
    (fun x => deriv (fun z => z ^ p * (1 - ε z)) x) =Θ[atTop] fun z => p * z ^ (p - 1) :=
      (isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn hp).isTheta
    _ =Θ[atTop] fun z => z ^ (p - 1) := IsTheta.const_mul_left hp <| isTheta_refl _ _

Похожие утверждения