isBigO_deriv_ofReal_cpow_const_atTop

English

In particular, the derivative of x ↦ x^{c} has Big-O rate at infinity comparable to x^{c.re-1}. If c = 0, the derivative is trivial constant. Otherwise, it is isBigO of x^{c.re-1}.

Русский

Пусть производная x ↦ x^{c} имеет скорость роста at infinity сопоставимую x^{c.re-1}. Если c=0, производная константна; иначе она имеет порядок Big-O относительно x^{c.re-1}.

LaTeX

$$$\\text{If }c\\in\\mathbb{C},\\ c\\neq 0:\\ \\mathrm{deriv}\\bigl(x\\mapsto x^{c}\\bigr)=O\\bigl(x^{c_{\\mathrm{re}}-1}\\bigr)\\text{ as }x\\to\\infty.$$$

Lean4

theorem isBigO_deriv_ofReal_cpow_const_atTop (c : ℂ) :
    deriv (fun (x : ℝ) => (x : ℂ) ^ c) =O[atTop] fun x => x ^ (c.re - 1) :=
  by
  obtain rfl | hc := eq_or_ne c 0
  · simp_rw [cpow_zero, deriv_const', Asymptotics.isBigO_zero]
  · exact (isTheta_deriv_ofReal_cpow_const_atTop hc).1

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