# 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} [] (P : Polynomial ๐) (hP : P โ  0) :
โแถ  (x : ๐) in Filter.atTop,
theorem Polynomial.isEquivalent_atTop_lead {๐ : Type u_1} [] (P : Polynomial ๐) [OrderTopology ๐] :
Asymptotics.IsEquivalent Filter.atTop (fun (x : ๐) => ) fun (x : ๐) =>
theorem Polynomial.tendsto_atTop_of_leadingCoeff_nonneg {๐ : Type u_1} [] (P : Polynomial ๐) [OrderTopology ๐] (hdeg : ) (hnng : ) :
Filter.Tendsto (fun (x : ๐) => ) Filter.atTop Filter.atTop
theorem Polynomial.tendsto_atTop_iff_leadingCoeff_nonneg {๐ : Type u_1} [] (P : Polynomial ๐) [OrderTopology ๐] :
Filter.Tendsto (fun (x : ๐) => ) Filter.atTop Filter.atTop โ
theorem Polynomial.tendsto_atBot_iff_leadingCoeff_nonpos {๐ : Type u_1} [] (P : Polynomial ๐) [OrderTopology ๐] :
Filter.Tendsto (fun (x : ๐) => ) Filter.atTop Filter.atBot โ
theorem Polynomial.tendsto_atBot_of_leadingCoeff_nonpos {๐ : Type u_1} [] (P : Polynomial ๐) [OrderTopology ๐] (hdeg : ) (hnps : ) :
Filter.Tendsto (fun (x : ๐) => ) Filter.atTop Filter.atBot
theorem Polynomial.abs_tendsto_atTop {๐ : Type u_1} [] (P : Polynomial ๐) [OrderTopology ๐] (hdeg : ) :
Filter.Tendsto (fun (x : ๐) => ||) Filter.atTop Filter.atTop
theorem Polynomial.abs_isBoundedUnder_iff {๐ : Type u_1} [] (P : Polynomial ๐) [OrderTopology ๐] :
(Filter.IsBoundedUnder (fun (x x_1 : ๐) => x โค x_1) Filter.atTop fun (x : ๐) => ||) โ
theorem Polynomial.abs_tendsto_atTop_iff {๐ : Type u_1} [] (P : Polynomial ๐) [OrderTopology ๐] :
Filter.Tendsto (fun (x : ๐) => ||) Filter.atTop Filter.atTop โ
theorem Polynomial.tendsto_nhds_iff {๐ : Type u_1} [] (P : Polynomial ๐) [OrderTopology ๐] {c : ๐} :
Filter.Tendsto (fun (x : ๐) => ) Filter.atTop (nhds c) โ
theorem Polynomial.isEquivalent_atTop_div {๐ : Type u_1} [] (P : Polynomial ๐) (Q : Polynomial ๐) [OrderTopology ๐] :
Asymptotics.IsEquivalent Filter.atTop (fun (x : ๐) => / ) fun (x : ๐) => * x ^ (โ - โ)
theorem Polynomial.div_tendsto_zero_of_degree_lt {๐ : Type u_1} [] (P : Polynomial ๐) (Q : Polynomial ๐) [OrderTopology ๐] (hdeg : ) :
Filter.Tendsto (fun (x : ๐) => / ) Filter.atTop (nhds 0)
theorem Polynomial.div_tendsto_zero_iff_degree_lt {๐ : Type u_1} [] (P : Polynomial ๐) (Q : Polynomial ๐) [OrderTopology ๐] (hQ : Q โ  0) :
Filter.Tendsto (fun (x : ๐) => / ) Filter.atTop (nhds 0) โ
theorem Polynomial.div_tendsto_leadingCoeff_div_of_degree_eq {๐ : Type u_1} [] (P : Polynomial ๐) (Q : Polynomial ๐) [OrderTopology ๐] (hdeg : ) :
Filter.Tendsto (fun (x : ๐) => / ) Filter.atTop
theorem Polynomial.div_tendsto_atTop_of_degree_gt' {๐ : Type u_1} [] (P : Polynomial ๐) (Q : Polynomial ๐) [OrderTopology ๐] (hdeg : ) (hpos : ) :
Filter.Tendsto (fun (x : ๐) => / ) Filter.atTop Filter.atTop
theorem Polynomial.div_tendsto_atTop_of_degree_gt {๐ : Type u_1} [] (P : Polynomial ๐) (Q : Polynomial ๐) [OrderTopology ๐] (hdeg : ) (hQ : Q โ  0) (hnng : ) :
Filter.Tendsto (fun (x : ๐) => / ) Filter.atTop Filter.atTop
theorem Polynomial.div_tendsto_atBot_of_degree_gt' {๐ : Type u_1} [] (P : Polynomial ๐) (Q : Polynomial ๐) [OrderTopology ๐] (hdeg : ) (hneg : ) :
Filter.Tendsto (fun (x : ๐) => / ) Filter.atTop Filter.atBot
theorem Polynomial.div_tendsto_atBot_of_degree_gt {๐ : Type u_1} [] (P : Polynomial ๐) (Q : Polynomial ๐) [OrderTopology ๐] (hdeg : ) (hQ : Q โ  0) (hnps : ) :
Filter.Tendsto (fun (x : ๐) => / ) Filter.atTop Filter.atBot
theorem Polynomial.abs_div_tendsto_atTop_of_degree_gt {๐ : Type u_1} [] (P : Polynomial ๐) (Q : Polynomial ๐) [OrderTopology ๐] (hdeg : ) (hQ : Q โ  0) :
Filter.Tendsto (fun (x : ๐) => | / |) Filter.atTop Filter.atTop
theorem Polynomial.isBigO_of_degree_le {๐ : Type u_1} [] (P : Polynomial ๐) (Q : Polynomial ๐) [OrderTopology ๐] (h : ) :
(fun (x : ๐) => ) =O[Filter.atTop] fun (x : ๐) =>