div_tendsto_atBot_of_degree_gt — Mathlib

English

If deg Q < deg P and P.leadingCoeff / Q.leadingCoeff < 0, then P(x)/Q(x) → −∞ as x → ∞.

Русский

Если deg Q < deg P и отношение ведущих коэффициентов отрицательно, то P(x)/Q(x) → −∞ при x → ∞.

LaTeX

$$$$\deg Q < \deg P,\; Q \neq 0,\; \frac{\text{leadingCoeff}(P)}{\text{leadingCoeff}(Q)} < 0 \Rightarrow \lim_{x\to\infty} \frac{P(x)}{Q(x)} = -\infty.$$$$

Lean4

theorem div_tendsto_atBot_of_degree_gt (hdeg : Q.degree < P.degree) (hQ : Q ≠ 0)
    (hnps : P.leadingCoeff / Q.leadingCoeff ≤ 0) : Tendsto (fun x => eval x P / eval x Q) atTop atBot :=
  have ratio_neg : P.leadingCoeff / Q.leadingCoeff < 0 :=
    lt_of_le_of_ne hnps
      (div_ne_zero (fun h => ne_zero_of_degree_gt hdeg <| leadingCoeff_eq_zero.mp h) fun h =>
        hQ <| leadingCoeff_eq_zero.mp h)
  div_tendsto_atBot_of_degree_gt' P Q hdeg ratio_neg

Похожие утверждения