linearGrowthSup_eventually_monotone

English

Let u, v be functions from natural numbers to extended reals. If u(n) ≤ v(n) for all sufficiently large n, then the linear growth supremums satisfy linearGrowthSup(u) ≤ linearGrowthSup(v).

Русский

Пусть u, v: ℕ → EReal. Если существует N such that для всех n ≥ N выполняется u(n) ≤ v(n), то линейно-пределяющие верхние пределы удовлетворяют неравенству linearGrowthSup(u) ≤ linearGrowthSup(v).

LaTeX

$$$\left(\exists N \in \mathbb{N}, \forall n \ge N:\; u(n) \le v(n)\right) \implies \operatorname{linearGrowthSup}(u) \le \operatorname{linearGrowthSup}(v).$$$

Lean4

theorem linearGrowthSup_eventually_monotone (h : u ≤ᶠ[atTop] v) : linearGrowthSup u ≤ linearGrowthSup v :=
  limsup_le_limsup (h.mono fun n u_v ↦ monotone_div_right_of_nonneg n.cast_nonneg' u_v)

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