Asymptotics of polynomial and rational functions

This file proves basic facts about the asymptotics of of polynomial and rational functions. The main result is Polynomial.isEquivalent_atTop_lead, which states that for any polynomial P of degree n with leading coefficient a, the corresponding polynomial function is equivalent to a * x^n as x goes to +∞.

theorem Polynomial.isEquivalent_atTop_lead {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] : Asymptotics.IsEquivalent Filter.atTop (fun (x : 𝕜) => eval x P) fun (x : 𝕜) => P.leadingCoeff * x ^ P.natDegree

theorem Polynomial.isEquivalent_atBot_lead {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] : Asymptotics.IsEquivalent Filter.atBot (fun (x : 𝕜) => eval x P) fun (x : 𝕜) => P.leadingCoeff * x ^ P.natDegree

theorem Polynomial.isEquivalent_atTop_div {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] : Asymptotics.IsEquivalent Filter.atTop (fun (x : 𝕜) => eval x P / eval x Q) fun (x : 𝕜) => P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

theorem Polynomial.isEquivalent_atBot_div {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] : Asymptotics.IsEquivalent Filter.atBot (fun (x : 𝕜) => eval x P / eval x Q) fun (x : 𝕜) => P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

theorem Polynomial.isLittleO_atTop_of_degree_lt {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (h : P.degree < Q.degree) : (fun (x : 𝕜) => eval x P) =o[Filter.atTop] fun (x : 𝕜) => eval x Q

theorem Polynomial.isLittleO_atBot_of_degree_lt {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (h : P.degree < Q.degree) : (fun (x : 𝕜) => eval x P) =o[Filter.atBot] fun (x : 𝕜) => eval x Q

theorem Polynomial.isBigO_atTop_of_degree_le {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (h : P.degree ≤ Q.degree) : (fun (x : 𝕜) => eval x P) =O[Filter.atTop] fun (x : 𝕜) => eval x Q

theorem Polynomial.isBigO_atBot_of_degree_le {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (h : P.degree ≤ Q.degree) : (fun (x : 𝕜) => eval x P) =O[Filter.atBot] fun (x : 𝕜) => eval x Q

theorem Polynomial.isEquivalent_cobounded_leading_monomial {R : Type u_2} [NormedRing R] [NormMulClass R] {P : Polynomial R} : Asymptotics.IsEquivalent (Bornology.cobounded R) (fun (x : R) => eval x P) fun (x : R) => P.leadingCoeff * x ^ P.natDegree

theorem Polynomial.isBigO_cobounded_pow_natDegree {R : Type u_2} [NormedRing R] [NormMulClass R] (p : Polynomial R) : (fun (x : R) => eval x p) =O[Bornology.cobounded R] fun (x : R) => x ^ p.natDegree

theorem Polynomial.isLittleO_cobounded_of_degree_lt {R : Type u_2} [NormedRing R] [NormMulClass R] {P Q : Polynomial R} (h : P.degree < Q.degree) : (fun (x : R) => eval x P) =o[Bornology.cobounded R] fun (x : R) => eval x Q

theorem Polynomial.isBigO_cobounded_of_degree_le {R : Type u_2} [NormedRing R] [NormMulClass R] {P Q : Polynomial R} (h : P.degree ≤ Q.degree) : (fun (x : R) => eval x P) =O[Bornology.cobounded R] fun (x : R) => eval x Q

theorem Polynomial.finite_abs_eval_le_of_degree_lt {P Q : Polynomial ℤ} (h : Q.degree < P.degree) : {x : ℤ | |eval x P| ≤ |eval x Q|}.Finite

If deg Q < deg P, there are only finitely many integers x where |P(x)| ≤ |Q(x)|.

theorem Polynomial.dvd_of_infinite_eval_dvd_eval {P Q : Polynomial ℤ} (mQ : Q.Monic) (h : {a : ℤ | eval a Q ∣ eval a P}.Infinite) : Q ∣ P

If Q(x) ∣ P(x) at infinitely many integers x and Q is monic, Q ∣ P.