Limits related to polynomial and rational functions

This file proves basic facts about limits of polynomial and rationals functions. The main result is eval_is_equivalent_at_top_eval_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_no_roots {𝕜 : Type u_1} [NormedLinearOrderedField 𝕜] (P : Polynomial 𝕜) (hP : P ≠ 0) : ∀ᶠ (x : 𝕜) in Filter.atTop, ¬P.IsRoot x

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

theorem Polynomial.tendsto_atTop_of_leadingCoeff_nonneg {𝕜 : Type u_1} [NormedLinearOrderedField 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : 0 < P.degree) (hnng : 0 ≤ P.leadingCoeff) : Filter.Tendsto (fun (x : 𝕜) => Polynomial.eval x P) Filter.atTop Filter.atTop

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

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

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

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

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

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

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

theorem Polynomial.isEquivalent_atTop_div {𝕜 : Type u_1} [NormedLinearOrderedField 𝕜] (P : Polynomial 𝕜) (Q : Polynomial 𝕜) [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)

theorem Polynomial.div_tendsto_zero_of_degree_lt {𝕜 : Type u_1} [NormedLinearOrderedField 𝕜] (P : Polynomial 𝕜) (Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : P.degree < Q.degree) : Filter.Tendsto (fun (x : 𝕜) => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop (nhds 0)

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

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

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

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

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

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

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

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