div_tendsto_leadingCoeff_div_of_degree_eq

English

If deg P = deg Q, then lim_{x→∞} P(x)/Q(x) = leadingCoeff(P)/leadingCoeff(Q).

Русский

Если deg P = deg Q, то предел P(x)/Q(x) при x→∞ равен leadingCoeff(P)/leadingCoeff(Q).

LaTeX

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

Lean4

theorem div_tendsto_leadingCoeff_div_of_degree_eq (hdeg : P.degree = Q.degree) :
    Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 <| P.leadingCoeff / Q.leadingCoeff) :=
  by
  refine (isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_
  rw [show (P.natDegree : ℤ) = Q.natDegree by simp [hdeg, natDegree]]
  simp

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