isTheta_deriv_rpow_p_mul_one_add_smoothingFn

English

The L2-norm of the derivative of z^p(1 − ε(z)) is Θ(z^{p−1}); more precisely, ||d/dz(z^p(1 − ε(z)))|| = Θ(z^{p−1}).

Русский

Норма Л2 производной z^p(1 − ε(z)) равна Θ(z^{p−1}); то есть ||d/dz(z^p(1 − ε(z)))|| = Θ(z^{p−1}).

LaTeX

$$$\\|\\frac{d}{dz}(z^p(1 - \\varepsilon(z)))\\| = Θ(z^{p-1}) \\quad (z \\to \\infty).$$$

Lean4

theorem isTheta_deriv_rpow_p_mul_one_add_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_add_smoothingFn hp).isTheta
    _ =Θ[atTop] fun z => z ^ (p - 1) := IsTheta.const_mul_left hp <| isTheta_refl _ _

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