English
Let u : N → [0, ∞) and a ∈ EReal. Then a ≤ expGrowthInf(u) if and only if for every b < a, there exists N such that for all n ≥ N, exp(b n) ≤ u(n).
Русский
Пусть u : N → [0, ∞) и a ∈ EReal. Тогда a ≤ expGrowthInf(u) если и только если для любого b < a существует N, такое что для всех n ≥ N выполняется exp(b n) ≤ u(n).
LaTeX
$$$a \le \expGrowthInf(u) \iff \forall b < a,\ (\exists N)\ \forall n \ge N,\ exp(b n) \le u(n)$$$
Lean4
theorem le_expGrowthInf_iff : a ≤ expGrowthInf u ↔ ∀ b < a, ∀ᶠ n : ℕ in atTop, exp (b * n) ≤ u n :=
by
rw [expGrowthInf, le_liminf_iff']
refine forall₂_congr fun b _ ↦ eventually_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
