# Documentation

Mathlib.Analysis.SpecialFunctions.Polynomials

# 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 : ) (hP : P 0) :
∀ᶠ (x : 𝕜) in Filter.atTop,
theorem Polynomial.isEquivalent_atTop_lead {𝕜 : Type u_1} (P : ) [] :
Asymptotics.IsEquivalent Filter.atTop (fun x => ) fun x =>
theorem Polynomial.tendsto_atTop_of_leadingCoeff_nonneg {𝕜 : Type u_1} (P : ) [] (hdeg : ) (hnng : ) :
Filter.Tendsto (fun x => ) Filter.atTop Filter.atTop
theorem Polynomial.tendsto_atTop_iff_leadingCoeff_nonneg {𝕜 : Type u_1} (P : ) [] :
Filter.Tendsto (fun x => ) Filter.atTop Filter.atTop
theorem Polynomial.tendsto_atBot_iff_leadingCoeff_nonpos {𝕜 : Type u_1} (P : ) [] :
Filter.Tendsto (fun x => ) Filter.atTop Filter.atBot
theorem Polynomial.tendsto_atBot_of_leadingCoeff_nonpos {𝕜 : Type u_1} (P : ) [] (hdeg : ) (hnps : ) :
Filter.Tendsto (fun x => ) Filter.atTop Filter.atBot
theorem Polynomial.abs_tendsto_atTop {𝕜 : Type u_1} (P : ) [] (hdeg : ) :
Filter.Tendsto (fun x => ||) Filter.atTop Filter.atTop
theorem Polynomial.abs_isBoundedUnder_iff {𝕜 : Type u_1} (P : ) [] :
(Filter.IsBoundedUnder (fun x x_1 => x x_1) Filter.atTop fun x => ||)
theorem Polynomial.abs_tendsto_atTop_iff {𝕜 : Type u_1} (P : ) [] :
Filter.Tendsto (fun x => ||) Filter.atTop Filter.atTop
theorem Polynomial.tendsto_nhds_iff {𝕜 : Type u_1} (P : ) [] {c : 𝕜} :
Filter.Tendsto (fun x => ) Filter.atTop (nhds c)
theorem Polynomial.isEquivalent_atTop_div {𝕜 : Type u_1} (P : ) (Q : ) [] :
Asymptotics.IsEquivalent Filter.atTop (fun x => / ) fun x => * x ^ ()
theorem Polynomial.div_tendsto_zero_of_degree_lt {𝕜 : Type u_1} (P : ) (Q : ) [] (hdeg : ) :
Filter.Tendsto (fun x => / ) Filter.atTop (nhds 0)
theorem Polynomial.div_tendsto_zero_iff_degree_lt {𝕜 : Type u_1} (P : ) (Q : ) [] (hQ : Q 0) :
Filter.Tendsto (fun x => / ) Filter.atTop (nhds 0)
theorem Polynomial.div_tendsto_leadingCoeff_div_of_degree_eq {𝕜 : Type u_1} (P : ) (Q : ) [] (hdeg : ) :
Filter.Tendsto (fun x => / ) Filter.atTop ()
theorem Polynomial.div_tendsto_atTop_of_degree_gt' {𝕜 : Type u_1} (P : ) (Q : ) [] (hdeg : ) (hpos : ) :
Filter.Tendsto (fun x => / ) Filter.atTop Filter.atTop
theorem Polynomial.div_tendsto_atTop_of_degree_gt {𝕜 : Type u_1} (P : ) (Q : ) [] (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 : ) (Q : ) [] (hdeg : ) (hneg : ) :
Filter.Tendsto (fun x => / ) Filter.atTop Filter.atBot
theorem Polynomial.div_tendsto_atBot_of_degree_gt {𝕜 : Type u_1} (P : ) (Q : ) [] (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 : ) (Q : ) [] (hdeg : ) (hQ : Q 0) :
Filter.Tendsto (fun x => | / |) Filter.atTop Filter.atTop
theorem Polynomial.isBigO_of_degree_le {𝕜 : Type u_1} (P : ) (Q : ) [] (h : ) :
(fun x => ) =O[Filter.atTop] fun x =>