expGrowthSup_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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