English
Let u : N → [0, ∞) and a ∈ EReal. Then expGrowthInf(u) ≤ a if and only if for every b > a, there are infinitely many n with u(n) ≤ exp(b n).
Русский
Пусть u : N → [0, ∞) и a ∈ EReal. Тогда expGrowthInf(u) ≤ a тогда и только если для каждого b > a существует бесконечное число n such that u(n) ≤ exp(b n).
LaTeX
$$$\expGrowthInf(u) \le a \iff \forall b > a,\ \exists^{\infty} n \in \mathbb{N},\ u(n) \le \exp(b n)$$$
Lean4
theorem expGrowthInf_le_iff : expGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ n : ℕ in atTop, u n ≤ exp (b * n) :=
by
rw [expGrowthInf, liminf_le_iff']
refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
rw [div_le_iff_le_mul (by norm_cast) (natCast_ne_top n), ← log_exp (n * b), mul_comm _ b]
exact logOrderIso.le_iff_le
