English
If deg Q < deg P and Q is nonzero with nonnegative sign of the leading coefficient ratio, then P(x)/Q(x) tends to +∞ 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_atTop_of_degree_gt (hdeg : Q.degree < P.degree) (hQ : Q ≠ 0)
(hnng : 0 ≤ P.leadingCoeff / Q.leadingCoeff) : Tendsto (fun x => eval x P / eval x Q) atTop atTop :=
have ratio_pos : 0 < P.leadingCoeff / Q.leadingCoeff :=
lt_of_le_of_ne hnng
(div_ne_zero (fun h => ne_zero_of_degree_gt hdeg <| leadingCoeff_eq_zero.mp h) fun h =>
hQ <| leadingCoeff_eq_zero.mp h).symm
div_tendsto_atTop_of_degree_gt' P Q hdeg ratio_pos
