le_expGrowthSup — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.Frequently.le_expGrowthSup (h : ∃ᶠ n : ℕ in atTop, exp (a * n) ≤ u n) : a ≤ expGrowthSup u :=
  le_expGrowthSup_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' <| by gcongr

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