le_expGrowthInf — Mathlib

English

If eventually exp(a n) ≤ u(n), then a ≤ expGrowthInf(u).

Русский

Если в конце концов выполняется exp(a n) ≤ u(n), тогда a ≤ expGrowthInf(u).

LaTeX

$$$\forall n \gg 0,\ exp(a n) \le u(n) \Rightarrow a \le \expGrowthInf(u)$$$

Lean4

theorem _root_.Eventually.le_expGrowthInf (h : ∀ᶠ n : ℕ in atTop, exp (a * n) ≤ u n) : a ≤ expGrowthInf u :=
  le_expGrowthInf_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' <| by gcongr

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