expGrowthInf_of_eventually_ge — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem expGrowthInf_of_eventually_ge (hb : b ≠ 0) (h : ∀ᶠ n in atTop, b * u n ≤ v n) :
    expGrowthInf u ≤ expGrowthInf v :=
  by
  apply (expGrowthInf_eventually_monotone h).trans' (le_expGrowthInf_mul.trans' _)
  rcases eq_top_or_lt_top b with rfl | b_top
  · rw [← Pi.top_def, expGrowthInf_top]
    exact le_add_of_nonneg_left le_top
  · rw [expGrowthInf_const hb b_top.ne, zero_add]

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