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, ¬Polynomial.IsRoot P 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 : 𝕜) => Polynomial.leadingCoeff P * x ^ Polynomial.natDegree P

theorem Polynomial.tendsto_atTop_of_leadingCoeff_nonneg {𝕜 : Type u_1} [NormedLinearOrderedField 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : 0 < Polynomial.degree P) (hnng : 0 ≤ Polynomial.leadingCoeff P) : 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 < Polynomial.degree P ∧ 0 ≤ Polynomial.leadingCoeff P

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 < Polynomial.degree P ∧ Polynomial.leadingCoeff P ≤ 0

theorem Polynomial.tendsto_atBot_of_leadingCoeff_nonpos {𝕜 : Type u_1} [NormedLinearOrderedField 𝕜] (P : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : 0 < Polynomial.degree P) (hnps : Polynomial.leadingCoeff P ≤ 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 < Polynomial.degree P) : 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 (x x_1 : 𝕜) => x ≤ x_1) Filter.atTop fun (x : 𝕜) => |Polynomial.eval x P|) ↔ Polynomial.degree P ≤ 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 < Polynomial.degree P

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) ↔ Polynomial.leadingCoeff P = c ∧ Polynomial.degree P ≤ 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 : 𝕜) => Polynomial.leadingCoeff P / Polynomial.leadingCoeff Q * x ^ (↑(Polynomial.natDegree P) - ↑(Polynomial.natDegree Q))

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

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

theorem Polynomial.div_tendsto_atTop_of_degree_gt' {𝕜 : Type u_1} [NormedLinearOrderedField 𝕜] (P : Polynomial 𝕜) (Q : Polynomial 𝕜) [OrderTopology 𝕜] (hdeg : Polynomial.degree Q < Polynomial.degree P) (hpos : 0 < Polynomial.leadingCoeff P / Polynomial.leadingCoeff Q) : 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 : Polynomial.degree Q < Polynomial.degree P) (hQ : Q ≠ 0) (hnng : 0 ≤ Polynomial.leadingCoeff P / Polynomial.leadingCoeff Q) : 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 : Polynomial.degree Q < Polynomial.degree P) (hneg : Polynomial.leadingCoeff P / Polynomial.leadingCoeff Q < 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 : Polynomial.degree Q < Polynomial.degree P) (hQ : Q ≠ 0) (hnps : Polynomial.leadingCoeff P / Polynomial.leadingCoeff Q ≤ 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 : Polynomial.degree Q < Polynomial.degree P) (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 : Polynomial.degree P ≤ Polynomial.degree Q) : (fun (x : 𝕜) => Polynomial.eval x P) =O[Filter.atTop] fun (x : 𝕜) => Polynomial.eval x Q