expGrowthSup_le_of_eventually_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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