English
For Q ≠ 0, lim_{x→∞} P(x)/Q(x) = 0 if and only if deg P < deg Q.
Русский
Для Q ≠ 0, lim_{x→∞} P(x)/Q(x) = 0 тогда и только тогда, когда deg P < deg Q.
LaTeX
$$$$\text{Tendsto}_{x\to\infty}\bigl( \tfrac{P(x)}{Q(x)} \bigr) = 0 \iff \deg P < \deg Q\quad (Q \neq 0). $$$$
Lean4
theorem div_tendsto_zero_iff_degree_lt (hQ : Q ≠ 0) :
Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0) ↔ P.degree < Q.degree :=
by
refine ⟨fun h => ?_, div_tendsto_zero_of_degree_lt P Q⟩
by_cases hPQ : P.leadingCoeff / Q.leadingCoeff = 0
· simp only [div_eq_mul_inv, inv_eq_zero, mul_eq_zero] at hPQ
rcases hPQ with hP0 | hQ0
· rw [leadingCoeff_eq_zero.1 hP0, degree_zero]
exact bot_lt_iff_ne_bot.2 fun hQ' => hQ (degree_eq_bot.1 hQ')
· exact absurd (leadingCoeff_eq_zero.1 hQ0) hQ
· have := (isEquivalent_atTop_div P Q).tendsto_nhds h
rw [tendsto_const_mul_zpow_atTop_nhds_iff hPQ] at this
rcases this with h | h
· exact absurd h.2 hPQ
· rw [sub_lt_iff_lt_add, zero_add, Int.ofNat_lt] at h
exact degree_lt_degree h.1
