frequently_exp_le — Mathlib

English

If a < expGrowthSup u, then there are infinitely many n with exp(a n) ≤ u(n).

Русский

Если a < expGrowthSup(u), тогда бесконечно много n удовлетворяют exp(a n) ≤ u(n).

LaTeX

$$$a < \expGrowthSup(u) \Rightarrow \exists^{\infty} n \in \mathbb{N},\ \exp(a n) \le u(n)$$$

Lean4

theorem frequently_exp_le (h : a < expGrowthSup u) : ∃ᶠ n : ℕ in atTop, exp (a * n) ≤ u n :=
  le_expGrowthSup_iff.1 (le_refl (expGrowthSup u)) a h

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