expGrowthInf_le — Mathlib

English

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

Русский

Если существует бесконечно много n, таких что u(n) ≤ exp(a n), то expGrowthInf(u) ≤ a.

LaTeX

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

Lean4

theorem _root_.Frequently.expGrowthInf_le (h : ∃ᶠ n : ℕ in atTop, u n ≤ exp (a * n)) : expGrowthInf u ≤ a :=
  by
  apply expGrowthInf_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans ?_
  gcongr

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