expGrowthSup_of_eventually_ge — Mathlib

English

Let hb ≠ 0 and h: ∀ᶠ n in atTop, b·u_n ≤ v_n. Then expGrowthSup(u) ≤ expGrowthSup(v).

Русский

Пусть hb ≠ 0 и ∀ᶠ n, b·u_n ≤ v_n. Тогда expGrowthSup(u) ≤ expGrowthSup(v).

LaTeX

$$$\text{hb: } b \neq 0 \;\land\; (b \cdot u_n \le v_n) \text{ eventually } \Rightarrow \expGrowthSup(u) \le \expGrowthSup(v)$$$

Lean4

theorem expGrowthSup_of_eventually_ge (hb : b ≠ 0) (h : ∀ᶠ n in atTop, b * u n ≤ v n) :
    expGrowthSup u ≤ expGrowthSup v :=
  by
  apply (expGrowthSup_eventually_monotone h).trans' (le_expGrowthSup_mul'.trans' _)
  rcases eq_top_or_lt_top b with rfl | b_top
  · exact expGrowthInf_top ▸ le_add_of_nonneg_left le_top
  · rw [expGrowthInf_const hb b_top.ne, zero_add]

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