isBigO_deriv_rpow_const_atTop — Mathlib

English

For a real p, the derivative of x^p is O(x^{p−1}) as x → ∞; in particular, the derivative is bounded up to a constant multiple of x^{p−1} at infinity.

Русский

Для любого p производная x^p есть O(x^{p−1}) при x→∞; то есть она ограничена сверху константой на множествах больших x и ведет себя как константа множителя x^{p−1}.

LaTeX

$$$\\displaystyle \\mathrm{deriv}(x^p) =O_{x\\to\\infty} x^{p-1}$$$

Lean4

theorem isBigO_deriv_rpow_const_atTop (p : ℝ) : deriv (fun (x : ℝ) => x ^ p) =O[atTop] fun x => x ^ (p - 1) :=
  by
  rcases eq_or_ne p 0 with rfl | hp
  case inl => simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]
  case inr => exact (isTheta_deriv_rpow_const_atTop hp).1

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