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