Limits related to polynomial and rational functions

This file proves basic facts about limits 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 +∞.

We can then use this result to prove various limits for polynomial and rational functions, depending on the degrees and leading coefficients of the considered polynomials.

theorem Polynomial.eventually_atTop_not_isRoot {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) (hP : P ≠ 0) : ∀ᶠ (x : 𝕜) in Filter.atTop, ¬P.IsRoot x

theorem Polynomial.eventually_atBot_not_isRoot {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) (hP : P ≠ 0) : ∀ᶠ (x : 𝕜) in Filter.atBot, ¬P.IsRoot x

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.tendsto_atTop_of_leadingCoeff_nonneg {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : 0 < P.degree) (hnng : 0 ≤ P.leadingCoeff) : Filter.Tendsto (fun (x : 𝕜) => eval x P) Filter.atTop Filter.atTop

theorem Polynomial.tendsto_atTop_iff_leadingCoeff_nonneg {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] : Filter.Tendsto (fun (x : 𝕜) => eval x P) Filter.atTop Filter.atTop ↔ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

theorem Polynomial.tendsto_atBot_iff_leadingCoeff_nonpos {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] : Filter.Tendsto (fun (x : 𝕜) => eval x P) Filter.atTop Filter.atBot ↔ 0 < P.degree ∧ P.leadingCoeff ≤ 0

theorem Polynomial.tendsto_atBot_of_leadingCoeff_nonpos {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : 0 < P.degree) (hnps : P.leadingCoeff ≤ 0) : Filter.Tendsto (fun (x : 𝕜) => eval x P) Filter.atTop Filter.atBot

theorem Polynomial.abs_tendsto_atTop {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : 0 < P.degree) : Filter.Tendsto (fun (x : 𝕜) => |eval x P|) Filter.atTop Filter.atTop

theorem Polynomial.isBoundedUnder_abs_atTop_iff {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] : (Filter.IsBoundedUnder (fun (x1 x2 : 𝕜) => x1 ≤ x2) Filter.atTop fun (x : 𝕜) => |eval x P|) ↔ P.degree ≤ 0

theorem Polynomial.abs_tendsto_atTop_iff {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] : Filter.Tendsto (fun (x : 𝕜) => |eval x P|) Filter.atTop Filter.atTop ↔ 0 < P.degree

theorem Polynomial.tendsto_nhds_iff {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] {c : 𝕜} : Filter.Tendsto (fun (x : 𝕜) => eval x P) Filter.atTop (nhds c) ↔ P.leadingCoeff = c ∧ P.degree ≤ 0

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.abs_tendsto_atBot {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : 0 < P.degree) : Filter.Tendsto (fun (x : 𝕜) => |eval x P|) Filter.atBot Filter.atTop

theorem Polynomial.isBoundedUnder_abs_atBot_iff {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] : (Filter.IsBoundedUnder (fun (x1 x2 : 𝕜) => x1 ≤ x2) Filter.atBot fun (x : 𝕜) => |eval x P|) ↔ P.degree ≤ 0

theorem Polynomial.abs_tendsto_atBot_iff {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] : Filter.Tendsto (fun (x : 𝕜) => |eval x P|) Filter.atBot Filter.atTop ↔ 0 < P.degree

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.div_tendsto_atTop_zero_of_degree_lt {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : P.degree < Q.degree) : Filter.Tendsto (fun (x : 𝕜) => eval x P / eval x Q) Filter.atTop (nhds 0)

theorem Polynomial.div_tendsto_atTop_zero_iff_degree_lt {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hQ : Q ≠ 0) : Filter.Tendsto (fun (x : 𝕜) => eval x P / eval x Q) Filter.atTop (nhds 0) ↔ P.degree < Q.degree

theorem Polynomial.div_tendsto_atTop_leadingCoeff_div_of_degree_eq {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : P.degree = Q.degree) : Filter.Tendsto (fun (x : 𝕜) => eval x P / eval x Q) Filter.atTop (nhds (P.leadingCoeff / Q.leadingCoeff))

theorem Polynomial.div_tendsto_atTop_of_degree_gt' {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : Q.degree < P.degree) (hpos : 0 < P.leadingCoeff / Q.leadingCoeff) : Filter.Tendsto (fun (x : 𝕜) => eval x P / eval x Q) Filter.atTop Filter.atTop

theorem Polynomial.div_tendsto_atTop_of_degree_gt {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : Q.degree < P.degree) (hQ : Q ≠ 0) (hnng : 0 ≤ P.leadingCoeff / Q.leadingCoeff) : Filter.Tendsto (fun (x : 𝕜) => eval x P / eval x Q) Filter.atTop Filter.atTop

theorem Polynomial.div_tendsto_atBot_of_degree_gt' {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : Q.degree < P.degree) (hneg : P.leadingCoeff / Q.leadingCoeff < 0) : Filter.Tendsto (fun (x : 𝕜) => eval x P / eval x Q) Filter.atTop Filter.atBot

theorem Polynomial.div_tendsto_atBot_of_degree_gt {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : Q.degree < P.degree) (hQ : Q ≠ 0) (hnps : P.leadingCoeff / Q.leadingCoeff ≤ 0) : Filter.Tendsto (fun (x : 𝕜) => eval x P / eval x Q) Filter.atTop Filter.atBot

theorem Polynomial.abs_div_tendsto_atTop_atTop_of_degree_gt {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : Q.degree < P.degree) (hQ : Q ≠ 0) : Filter.Tendsto (fun (x : 𝕜) => |eval x P / eval x Q|) Filter.atTop Filter.atTop

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.div_tendsto_atBot_zero_of_degree_lt {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : P.degree < Q.degree) : Filter.Tendsto (fun (x : 𝕜) => eval x P / eval x Q) Filter.atBot (nhds 0)

theorem Polynomial.div_tendsto_atBot_zero_iff_degree_lt {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hQ : Q ≠ 0) : Filter.Tendsto (fun (x : 𝕜) => eval x P / eval x Q) Filter.atBot (nhds 0) ↔ P.degree < Q.degree

theorem Polynomial.div_tendsto_atBot_leadingCoeff_div_of_degree_eq {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : P.degree = Q.degree) : Filter.Tendsto (fun (x : 𝕜) => eval x P / eval x Q) Filter.atBot (nhds (P.leadingCoeff / Q.leadingCoeff))

theorem Polynomial.abs_div_tendsto_atBot_atTop_of_degree_gt {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : Q.degree < P.degree) (hQ : Q ≠ 0) : Filter.Tendsto (fun (x : 𝕜) => |eval x P / eval x Q|) Filter.atBot Filter.atTop

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.