English
If a sequence u: ℕ → EReal is monotone and not identically bottom (not the least element), then its linearGrowthInf is nonnegative: linearGrowthInf(u) ≥ 0.
Русский
Если последовательность u: ℕ → EReal монотонна и не тождественно равна нижнему элементу, то её нижний линейный рост неотрицателен: linearGrowthInf(u) ≥ 0.
LaTeX
$$$0 \le \operatorname{linearGrowthInf}(u)$$$
Lean4
theorem _root_.Monotone.linearGrowthInf_nonneg (h : Monotone u) (h' : u ≠ ⊥) : 0 ≤ linearGrowthInf u :=
by
simp only [ne_eq, funext_iff, not_forall] at h'
obtain ⟨m, hm⟩ := h'
have m_n : ∀ᶠ n in atTop, u m ≤ u n := eventually_atTop.2 ⟨m, fun _ hb ↦ h hb⟩
rcases eq_or_ne (u m) ⊤ with hm' | hm'
· rw [hm'] at m_n
exact le_top.trans (linearGrowthInf_top.symm.trans_le (linearGrowthInf_eventually_monotone m_n))
· rw [← linearGrowthInf_const hm hm']
exact linearGrowthInf_eventually_monotone m_n
