isTheta_deriv_rpow_const_atTop — Mathlib

English

For p ≠ 0, the derivative of x^p satisfies is Theta at infinity: there holds deriv(x^p) =_Θ x^{p−1} as x → ∞.

Русский

Для p ≠ 0 производная функции x^p ведет себя как Θ(x^{p−1}) при x → ∞. То есть производная растет пропорционально x^{p−1}.

LaTeX

$$$\\displaystyle \\operatorname{deriv}(x^p) =Θ\\_{x\\to\\infty} x^{p-1} \\quad (p\\neq 0)$$$

Lean4

theorem isTheta_deriv_rpow_const_atTop {p : ℝ} (hp : p ≠ 0) :
    deriv (fun (x : ℝ) => x ^ p) =Θ[atTop] fun x => x ^ (p - 1) := by
  calc
    deriv (fun (x : ℝ) => x ^ p) =ᶠ[atTop] fun x => p * x ^ (p - 1) :=
      by
      filter_upwards [eventually_ne_atTop 0] with x hx
      rw [Real.deriv_rpow_const (Or.inl hx)]
    _ =Θ[atTop] fun x => x ^ (p - 1) := Asymptotics.IsTheta.const_mul_left hp Asymptotics.isTheta_rfl

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