English
Let f be polynomially growing. Then one of the three alternatives holds asymptotically: f(x) = 0 eventually, or f(x) > 0 eventually, or f(x) < 0 eventually.
Русский
Пусть f: ℝ → ℝ растёт полиномиально. Тогда асимптотически выполняется одно из трёх: f(x) становится нулём, или становится положительной, или становится отрицательной.
LaTeX
$$$\\text{GrowsPolynomially}(f) \\Rightarrow \\left( \\forall^\\infty x \\in atTop,\; f(x) = 0 \\right) \\lor \\left( \\forall^\\infty x \\in atTop,\; f(x) > 0 \\right) \\lor \\left( \\forall^\\infty x \\in atTop,\; f(x) < 0 \\right)$$$
Lean4
theorem eventually_atTop_zero_or_pos_or_neg (hf : GrowsPolynomially f) :
(∀ᶠ x in atTop, f x = 0) ∨ (∀ᶠ x in atTop, 0 < f x) ∨ (∀ᶠ x in atTop, f x < 0) := by
if h : ∃ᶠ x in atTop, f x = 0 then exact Or.inl <| eventually_zero_of_frequently_zero hf h
else
rw [not_frequently] at h
push_neg at h
cases eventually_atTop_nonneg_or_nonpos hf with
| inl h' =>
refine Or.inr (Or.inl ?_)
simp only [lt_iff_le_and_ne]
rw [eventually_and]
exact ⟨h', by filter_upwards [h] with x hx; exact hx.symm⟩
| inr h' =>
refine Or.inr (Or.inr ?_)
simp only [lt_iff_le_and_ne]
rw [eventually_and]
exact ⟨h', h⟩
