Polynomial.isEquivalent_atTop_div
theorem Polynomial.isEquivalent_atTop_div :
∀ {𝕜 : Type u_1} [inst : NormedLinearOrderedField 𝕜] (P Q : Polynomial 𝕜) [inst_1 : OrderTopology 𝕜],
Asymptotics.IsEquivalent Filter.atTop (fun x => Polynomial.eval x P / Polynomial.eval x Q) fun x =>
P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)
This theorem states that for any polynomials `P` and `Q` over a normed linearly ordered field `𝕜`, with an order topology, the function which evaluates `P` divided by `Q` at `x`, is asymptotically equivalent (as `x` approaches infinity) to the function that is the product of the leading coefficient of `P` divided by the leading coefficient of `Q`, and `x` to the power of the difference of the natural degrees of `P` and `Q`. Essentially, this states that as `x` goes to infinity, the ratio of the evaluations of the two polynomials behaves like a power function where the exponent is the difference between the degrees of the two polynomials and the constant is the ratio of their leading coefficients.
More concisely: For polynomials `P` and `Q` over a normed linearly ordered field with order topology, as `x` approaches infinity, the ratio of `P x / Q x` are asymptotically equivalent to the product of the leading coefficients quotient and `x` raised to the power of the difference of degrees of `P` and `Q`.
|
Polynomial.isEquivalent_atTop_lead
theorem Polynomial.isEquivalent_atTop_lead :
∀ {𝕜 : Type u_1} [inst : NormedLinearOrderedField 𝕜] (P : Polynomial 𝕜) [inst_1 : OrderTopology 𝕜],
Asymptotics.IsEquivalent Filter.atTop (fun x => Polynomial.eval x P) fun x => P.leadingCoeff * x ^ P.natDegree
This theorem states that for any polynomial `P` over a normed linearly ordered field `𝕜` with an order topology, the evaluation of the polynomial at a value `x` is asymptotically equivalent to the product of the polynomial's leading coefficient and `x` raised to the power of the polynomial's degree, as `x` goes to infinity. In simpler terms, as `x` grows without bound, the behavior of the polynomial `P` is dominated by its term with the highest degree.
More concisely: For any polynomial `P` over a normed linearly ordered field `𝕜`, as `x` approaches infinity, `P x` is asymptotically equivalent to the product of `P`'s leading coefficient and `x` raised to the power of `P`'s degree.
|