English
If deg Q < deg P, Q ≠ 0, and leadingCoeff(P)/leadingCoeff(Q) ≥ 0, then P(x)/Q(x) → ∞ as x → ∞.
Русский
Если deg Q < deg P, Q ≠ 0 и ведущий коэффициент отношения неотрицателен, то P(x)/Q(x) → ∞ при x → ∞.
LaTeX
$$$$\deg Q < \deg P,\; Q \neq 0,\; 0 \le \frac{\text{leadingCoeff}(P)}{\text{leadingCoeff}(Q)} \Rightarrow \lim_{x\to\infty} \frac{P(x)}{Q(x)} = +\infty.$$$$
Lean4
theorem div_tendsto_atBot_of_degree_gt' (hdeg : Q.degree < P.degree) (hneg : P.leadingCoeff / Q.leadingCoeff < 0) :
Tendsto (fun x => eval x P / eval x Q) atTop atBot :=
by
have hQ : Q ≠ 0 := fun h => by
simp only [h, div_zero, leadingCoeff_zero] at hneg
exact hneg.false
rw [← natDegree_lt_natDegree_iff hQ] at hdeg
refine (isEquivalent_atTop_div P Q).symm.tendsto_atBot ?_
apply Tendsto.const_mul_atTop_of_neg hneg
apply tendsto_zpow_atTop_atTop
cutsat
