Behaviour at infinity of polynomial and rational functions

We prove basic facts about the behavior of polynomial and rational functions at infinity.

The main result is Polynomial.tendsTo_atTop_div_nhds_leadingCoeff, which states that, for any polynomial P of degree n with leading coefficient a, P / x ^ n → a as x → +∞.

We then use this result to characterise the behaviour at infinity of polynomials and rational functions in terms of their degrees and leading coefficients.

theorem Polynomial.tendsTo_atTop_div_nhds_leadingCoeff {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (P : Polynomial F) [TopologicalSpace F] [OrderTopology F] : Filter.Tendsto (fun (x : F) => eval x P / x ^ P.natDegree) Filter.atTop (nhds P.leadingCoeff)

theorem Polynomial.tendsTo_atTop_div_nhds_one {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {P : Polynomial F} [TopologicalSpace F] [OrderTopology F] (hP : P ≠ 0) : Filter.Tendsto (fun (x : F) => eval x P / (P.leadingCoeff * x ^ P.natDegree)) Filter.atTop (nhds 1)

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

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

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

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

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

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

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

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

theorem Polynomial.tendsTo_atBot_div_nhds_one {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {P : Polynomial F} [TopologicalSpace F] [OrderTopology F] (hP : P ≠ 0) : Filter.Tendsto (fun (x : F) => eval x P / (P.leadingCoeff * x ^ P.natDegree)) Filter.atBot (nhds 1)

theorem Polynomial.abs_tendsto_atBot {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {P : Polynomial F} (hdeg : 0 < P.degree) : Filter.Tendsto (fun (x : F) => |eval x P|) Filter.atBot Filter.atTop

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

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

theorem Polynomial.div_tendsTo_atTop_div_nhds_one {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {P Q : Polynomial F} [TopologicalSpace F] [OrderTopology F] (hP : P ≠ 0) (hQ : Q ≠ 0) : Filter.Tendsto (fun (x : F) => eval x P / eval x Q / (P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree))) Filter.atTop (nhds 1)

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

theorem Polynomial.div_tendsto_atTop_zero_of_degree_lt {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {P Q : Polynomial F} [TopologicalSpace F] [OrderTopology F] (hdeg : P.degree < Q.degree) : Filter.Tendsto (fun (x : F) => eval x P / eval x Q) Filter.atTop (nhds 0)

theorem Polynomial.div_tendsto_atTop_leadingCoeff_div_iff_degree_eq {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {P Q : Polynomial F} [TopologicalSpace F] [OrderTopology F] (hP : P ≠ 0) (hQ : Q ≠ 0) : Filter.Tendsto (fun (x : F) => eval x P / eval x Q) Filter.atTop (nhds (P.leadingCoeff / Q.leadingCoeff)) ↔ P.degree = Q.degree

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

theorem Polynomial.div_tendsto_atTop_iff_degree_gt {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {P Q : Polynomial F} (hQ : Q ≠ 0) : Filter.Tendsto (fun (x : F) => eval x P / eval x Q) Filter.atTop Filter.atTop ↔ Q.degree < P.degree ∧ 0 ≤ P.leadingCoeff / Q.leadingCoeff

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

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

theorem Polynomial.div_tendsto_atBot_iff_degree_gt {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {P Q : Polynomial F} (hQ : Q ≠ 0) : Filter.Tendsto (fun (x : F) => eval x P / eval x Q) Filter.atTop Filter.atBot ↔ Q.degree < P.degree ∧ P.leadingCoeff / Q.leadingCoeff ≤ 0

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

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

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

theorem Polynomial.div_tendsTo_atBot_div_nhds_one {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {P Q : Polynomial F} [TopologicalSpace F] [OrderTopology F] (hP : P ≠ 0) (hQ : Q ≠ 0) : Filter.Tendsto (fun (x : F) => eval x P / eval x Q / (P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree))) Filter.atBot (nhds 1)

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

theorem Polynomial.div_tendsto_atBot_zero_of_degree_lt {F : Type u_1} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {P Q : Polynomial F} [TopologicalSpace F] [OrderTopology F] (hdeg : P.degree < Q.degree) : Filter.Tendsto (fun (x : F) => eval x P / eval x Q) Filter.atBot (nhds 0)

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

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