English
If there exists a real bound b such that u(n) ≤ v(n) + b eventually, then linearGrowthInf u ≤ linearGrowthInf v.
Русский
Если существует число b, такое что u(n) ≤ v(n) + b не позднее некоторого момента, то нижний рост u не превышает нижний рост v.
LaTeX
$$$\text{hb}: b \neq \top \quad\land\; h: \forall^{\infty} n,\ u(n) \le v(n) + b \implies \operatorname{linearGrowthInf} u \le \operatorname{linearGrowthInf} v$$$
Lean4
theorem linearGrowthInf_le_of_eventually_le (hb : b ≠ ⊤) (h : ∀ᶠ n in atTop, u n ≤ v n + b) :
linearGrowthInf u ≤ linearGrowthInf v :=
by
apply (linearGrowthInf_eventually_monotone h).trans
rcases eq_bot_or_bot_lt b with rfl | b_bot
· simp only [add_bot, ← Pi.bot_def, linearGrowthInf_bot, bot_le]
· apply (linearGrowthInf_add_le' _ _).trans_eq <;> rw [linearGrowthSup_const b_bot.ne' hb]
· exact add_zero (linearGrowthInf v)
· exact Or.inr EReal.zero_ne_top
· exact Or.inr EReal.zero_ne_bot
