eventually_le_exp

Mathlib.Analysis.Asymptotics.ExpGrowth

URI: https://scilib.ai/kg/mathlib#ExpGrowth.eventually_le_exp

English

If expGrowthSup u < a, then u(n) ≤ exp(a n) for all sufficiently large n.

Русский

Если expGrowthSup(u) < a, то существует N such that для всех n ≥ N, u(n) ≤ exp(a n).

LaTeX

$$$\expGrowthSup(u) < a \Rightarrow \exists N \forall n \ge N,\ u(n) \le \exp(a n)$$$

Lean4

theorem eventually_le_exp (h : expGrowthSup u < a) : ∀ᶠ n : ℕ in atTop, u n ≤ exp (a * n) :=
  expGrowthSup_le_iff.1 (le_refl (expGrowthSup u)) a h

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

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

Разделы

Аффилиация

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