div_tendsto_atTop_of_degree_gt' — Mathlib

English

If deg P = deg Q, then the limit of P(x)/Q(x) as x → ∞ equals the ratio of leading coefficients.

Русский

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

LaTeX

$$$$\deg P = \deg Q \Rightarrow \lim_{x\to\infty} \frac{P(x)}{Q(x)} = \frac{\text{leadingCoeff}(P)}{\text{leadingCoeff}(Q)}.$$$$

Lean4

theorem div_tendsto_atTop_of_degree_gt' (hdeg : Q.degree < P.degree) (hpos : 0 < P.leadingCoeff / Q.leadingCoeff) :
    Tendsto (fun x => eval x P / eval x Q) atTop atTop :=
  by
  have hQ : Q ≠ 0 := fun h => by
    simp only [h, div_zero, leadingCoeff_zero] at hpos
    exact hpos.false
  rw [← natDegree_lt_natDegree_iff hQ] at hdeg
  refine (isEquivalent_atTop_div P Q).symm.tendsto_atTop ?_
  apply Tendsto.const_mul_atTop hpos
  apply tendsto_zpow_atTop_atTop
  cutsat

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