div_tendsto_zero_of_degree_lt — Mathlib

English

If deg P < deg Q, then P(x)/Q(x) → 0 as x → ∞ (with Q ≠ 0).

Русский

Если deg P < deg Q, то P(x)/Q(x)→0 при x→∞ (при Q ≠ 0).

LaTeX

$$$$\deg P < \deg Q \implies \lim_{x\to\infty} \frac{P(x)}{Q(x)} = 0.$$$

Lean4

theorem div_tendsto_zero_of_degree_lt (hdeg : P.degree < Q.degree) :
    Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0) :=
  by
  by_cases hP : P = 0
  · simp [hP]
  rw [← natDegree_lt_natDegree_iff hP] at hdeg
  refine (isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_
  rw [← mul_zero]
  refine (tendsto_zpow_atTop_zero ?_).const_mul _
  cutsat

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