expGrowthInf_le_expGrowthSup_of_frequently_le

English

Let u, v : N → [0, ∞]. If u(n) ≤ v(n) for infinitely many n, then the exponential growth rate of u does not exceed that of v, i.e. expGrowthInf(u) ≤ expGrowthSup(v).

Русский

Пусть u, v : N → [0, ∞]. Если не менее бесконечно часто выполняется u(n) ≤ v(n), тогда темп экспоненциального роста u не превосходит темп роста v: expGrowthInf(u) ≤ expGrowthSup(v).

LaTeX

$$$\bigl(\exists^{\infty} n \in \mathbb{N},\ u(n) \le v(n)\bigr) \Rightarrow \expGrowthInf(u) \le \expGrowthSup(v)$$$

Lean4

theorem expGrowthInf_le_expGrowthSup_of_frequently_le (h : ∃ᶠ n in atTop, u n ≤ v n) :
    expGrowthInf u ≤ expGrowthSup v :=
  liminf_le_limsup_of_frequently_le <| h.mono fun n u_v ↦ by gcongr

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