English
Let u : N → [0, ∞) and a ∈ EReal. Then expGrowthSup(u) ≤ a iff for every b > a, there are infinitely many n with u(n) ≤ exp(b n).
Русский
Пусть u : N → [0, ∞) и a ∈ EReal. Тогда expGrowthSup(u) ≤ a тогда и только если для каждого b > a существует бесконечное множество n such that u(n) ≤ exp(b n).
LaTeX
$$$\expGrowthSup(u) \le a \iff \forall b > a,\ \exists^{\infty} n \in \mathbb{N},\ u(n) \le \exp(b n)$$$
Lean4
theorem expGrowthSup_le_iff : expGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ n : ℕ in atTop, u n ≤ exp (b * n) :=
by
rw [expGrowthSup, limsup_le_iff']
refine forall₂_congr fun b _ ↦ eventually_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
