English
Let f be a function with polynomial growth. Then f is eventually either nonnegative or nonpositive; that is, either f(x) ≥ 0 for all sufficiently large x, or f(x) ≤ 0 for all sufficiently large x.
Русский
Пусть f: ℝ → ℝ растёт полиномиально. Тогда существует предел на бесконечности: либо f становится неотрицательной, либо неотрицательной становится f.
LaTeX
$$$\\text{GrowsPolynomially}(f) \\Rightarrow \\left( \\forall^\\infty x \\in atTop,\; 0 \\le f(x) \\right) \\lor \\left( \\forall^\\infty x \\in atTop,\; f(x) \\le 0 \\right)$$$
Lean4
theorem eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) :
(∀ᶠ x in atTop, 0 ≤ f x) ∨ (∀ᶠ x in atTop, f x ≤ 0) :=
by
obtain ⟨c₁, _, c₂, _, h⟩ := hf (1 / 2) (by norm_num)
match lt_trichotomy c₁ c₂ with
| .inl hlt => -- c₁ < c₂
left
filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg
have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
rw [Set.mem_Icc]
exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
have hu := hx (3 / 4 * x) h'
have hu := Set.nonempty_of_mem hu
rw [Set.nonempty_Icc] at hu
have hu' : 0 ≤ (c₂ - c₁) * f x := by linarith
exact nonneg_of_mul_nonneg_right hu' (by linarith)
| .inr (.inr hgt) => -- c₂ < c₁
right
filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg
have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
rw [Set.mem_Icc]
exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
have hu := hx (3 / 4 * x) h'
have hu := Set.nonempty_of_mem hu
rw [Set.nonempty_Icc] at hu
have hu' : (c₁ - c₂) * f x ≤ 0 := by linarith
exact nonpos_of_mul_nonpos_right hu' (by linarith)
| .inr (.inl heq) => -- c₁ = c₂
have hmain : ∃ c, ∀ᶠ x in atTop, f x = c :=
by
simp only [heq, Set.Icc_self, Set.mem_singleton_iff] at h
rw [eventually_atTop] at h
obtain ⟨n₀, hn₀⟩ := h
refine ⟨f (max n₀ 2), ?_⟩
rw [eventually_atTop]
refine ⟨max n₀ 2, ?_⟩
refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step
case base =>
intro x ⟨hxlb, hxub⟩
have h₁ :=
calc
n₀ ≤ 1 * max n₀ 2 := by simp
_ ≤ 2 * max n₀ 2 := by gcongr; norm_num
have h₂ := hn₀ (2 * max n₀ 2) h₁ (max n₀ 2) ⟨by simp, by linarith⟩
rw [h₂]
exact hn₀ (2 * max n₀ 2) h₁ x ⟨by simp [hxlb], le_of_lt hxub⟩
case step =>
intro n hn hyp_ind z hz
have z_nonneg : 0 ≤ z := by
calc
(0 : ℝ) ≤ (2 : ℝ) ^ n * max n₀ 2 := by exact mul_nonneg (pow_nonneg (by norm_num) _) (by norm_num)
_ ≤ z := by exact_mod_cast hz.1
have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 :=
by
nth_rewrite 1 [← one_mul (max n₀ 2)]
gcongr
exact one_le_pow₀ (by norm_num : (1 : ℝ) ≤ 2)
have n₀_le_z : n₀ ≤ z := by
calc
n₀ ≤ max n₀ 2 := by simp
_ ≤ (2 : ℝ) ^ n * max n₀ 2 := le_2n
_ ≤ _ := by exact_mod_cast hz.1
have fz_eq_c₂fz : f z = c₂ * f z := hn₀ z n₀_le_z z ⟨by linarith, le_rfl⟩
have z_to_half_z' : f (1 / 2 * z) = c₂ * f z := hn₀ z n₀_le_z (1 / 2 * z) ⟨le_rfl, by linarith⟩
have z_to_half_z : f (1 / 2 * z) = f z := by rwa [← fz_eq_c₂fz] at z_to_half_z'
have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) :=
by
refine hyp_ind (1 / 2 * z) ⟨?lb, ?ub⟩
case lb =>
calc
max n₀ 2 ≤ ((1 : ℝ) / (2 : ℝ)) * (2 : ℝ) ^ 1 * max n₀ 2 := by simp
_ ≤ ((1 : ℝ) / (2 : ℝ)) * (2 : ℝ) ^ n * max n₀ 2 := by gcongr; norm_num
_ ≤ _ := by rw [mul_assoc]; gcongr; exact_mod_cast hz.1
case
ub =>
have h₁ : (2 : ℝ) ^ n = ((1 : ℝ) / (2 : ℝ)) * (2 : ℝ) ^ (n + 1) :=
by
rw [one_div, pow_add, pow_one]
ring
rw [h₁, mul_assoc]
gcongr
exact_mod_cast hz.2
rw [← z_to_half_z, half_z_to_base]
obtain ⟨c, hc⟩ := hmain
cases le_or_gt 0 c with
| inl hpos => exact Or.inl <| by filter_upwards [hc] with _ hc; simpa only [hc]
| inr hneg =>
right
filter_upwards [hc] with x hc
exact le_of_lt <| by simpa only [hc]
