linearGrowthSup_le_of_eventually_le

English

If there exists a bound b with a certain eventual le property, then linearGrowthSup u ≤ linearGrowthSup v.

Русский

Если существует ограничение b с необходимым свойством, то верхний рост u не превосходит верхний рост v.

LaTeX

$$$\text{hb}: b \neq \top \;\land\; h: \forall^{\infty} n,\ u(n) \le v(n) + b \Rightarrow \operatorname{linearGrowthSup} u \le \operatorname{linearGrowthSup} v$$$

Lean4

theorem linearGrowthSup_le_of_eventually_le (hb : b ≠ ⊤) (h : ∀ᶠ n in atTop, u n ≤ v n + b) :
    linearGrowthSup u ≤ linearGrowthSup v :=
  by
  apply (linearGrowthSup_eventually_monotone h).trans
  rcases eq_bot_or_bot_lt b with rfl | b_bot
  · simp only [add_bot, ← Pi.bot_def, linearGrowthSup_bot, bot_le]
  · apply (linearGrowthSup_add_le _ _).trans_eq <;> rw [linearGrowthSup_const b_bot.ne' hb]
    · exact add_zero (linearGrowthSup v)
    · exact Or.inr EReal.zero_ne_top
    · exact Or.inr EReal.zero_ne_bot

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