English
As x → ∞, P(x)/Q(x) is asymptotically equivalent to (leadingCoeff P / leadingCoeff Q) · x^(deg P − deg Q).
Русский
При x → ∞ отношение P(x)/Q(x) асимптотически эквивалентно (LC(P)/LC(Q)) · x^(deg P − deg Q).
LaTeX
$$$$\frac{P(x)}{Q(x)} \sim \frac{\text{leadingCoeff}(P)}{\text{leadingCoeff}(Q)} \; x^{\deg P - \deg Q} \quad (x \to \infty). $$$$
Lean4
theorem isEquivalent_atTop_div :
(fun x => eval x P / eval x Q) ~[atTop] fun x =>
P.leadingCoeff / Q.leadingCoeff * x ^ (P.natDegree - Q.natDegree : ℤ) :=
by
by_cases hP : P = 0
· simp [hP, IsEquivalent.refl]
by_cases hQ : Q = 0
· simp [hQ, IsEquivalent.refl]
refine
(P.isEquivalent_atTop_lead.symm.div Q.isEquivalent_atTop_lead.symm).symm.trans
(EventuallyEq.isEquivalent ((eventually_gt_atTop 0).mono fun x hx => ?_))
simp [← div_mul_div_comm, zpow_sub₀ hx.ne.symm]
