expGrowthInf_le_of_eventually_le — Mathlib

English

If b ≠ ∞ and u ≤ b·v holds eventually, then expGrowthInf(u) ≤ expGrowthInf(v).

Русский

Если b ≠ ∞ и неравенство u ≤ b·v выполняется в пределе (в конечном смысле), то expGrowthInf(u) ≤ expGrowthInf(v).

LaTeX

$$$\text{hb: } b \neq \infty \;\land\; (u(n) \le b\,v(n)) \text{ eventually } \Rightarrow \expGrowthInf(u) \le \expGrowthInf(v)$$$

Lean4

theorem expGrowthInf_le_of_eventually_le (hb : b ≠ ∞) (h : ∀ᶠ n in atTop, u n ≤ b * v n) :
    expGrowthInf u ≤ expGrowthInf v :=
  by
  apply (expGrowthInf_eventually_monotone h).trans
  rcases eq_zero_or_pos b with rfl | b_pos
  · simp only [zero_mul, ← Pi.zero_def, expGrowthInf_zero, bot_le]
  · apply (expGrowthInf_mul_le _ _).trans_eq <;> rw [expGrowthSup_const b_pos.ne' hb]
    · exact zero_add (expGrowthInf v)
    · exact .inl zero_ne_bot
    · exact .inl zero_ne_top

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