English
Let P ∈ 𝕜[X]. The limit of P(x) as x → ∞ exists and equals c if and only if leadingCoeff(P) = c and deg P ≤ 0.
Русский
Пусть P ∈ 𝕜[X]. Предел P(x) при x → ∞ существует и равен c тогда и только тогда, когда leadingCoeff(P) = c и deg P ≤ 0.
LaTeX
$$$$\operatorname{Tendsto}\bigl( x \mapsto P(x) \bigr)_{x\to\infty} = c \iff \text{leadingCoeff}(P) = c \text{ and } \deg P \le 0.$$$$
Lean4
theorem tendsto_nhds_iff {c : 𝕜} : Tendsto (fun x => eval x P) atTop (𝓝 c) ↔ P.leadingCoeff = c ∧ P.degree ≤ 0 :=
by
refine ⟨fun h => ?_, fun h => ?_⟩
· have := P.isEquivalent_atTop_lead.tendsto_nhds h
by_cases hP : P.leadingCoeff = 0
· simp only [hP, zero_mul, tendsto_const_nhds_iff] at this
exact ⟨_root_.trans hP this, by simp [leadingCoeff_eq_zero.1 hP]⟩
· rw [tendsto_const_mul_pow_nhds_iff hP, natDegree_eq_zero_iff_degree_le_zero] at this
exact this.symm
· refine P.isEquivalent_atTop_lead.symm.tendsto_nhds ?_
have : P.natDegree = 0 := natDegree_eq_zero_iff_degree_le_zero.2 h.2
simp only [h.1, this, pow_zero, mul_one]
exact tendsto_const_nhds
