isLittleO_rpow_exp_atTop

Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

URI: https://scilib.ai/kg/mathlib#isLittleO_rpow_exp_atTop

← MathLib Explorer

English

For any s ∈ ℝ, x^s = o(exp x) as x → ∞.

Русский

Для любого s ∈ ℝ, x^s = o(exp x) при x → ∞.

LaTeX

$$$$ x^s = o(\exp x) \quad (x \to \infty) $$$$

Lean4

/-- `x ^ s = o(exp x)` as `x → ∞` for any real `s`. -/
theorem isLittleO_rpow_exp_atTop (s : ℝ) : (fun x : ℝ => x ^ s) =o[atTop] exp := by
  simpa only [one_mul] using isLittleO_rpow_exp_pos_mul_atTop s one_pos

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru