# mathlib3documentation

analysis.special_functions.polynomials

# Limits related to polynomial and rational functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :
theorem polynomial.is_equivalent_at_top_lead {𝕜 : Type u_1} (P : polynomial 𝕜)  :
(λ (x : 𝕜), P) (λ (x : 𝕜), P.leading_coeff * x ^ P.nat_degree)
theorem polynomial.tendsto_at_top_of_leading_coeff_nonneg {𝕜 : Type u_1} (P : polynomial 𝕜) (hdeg : 0 < P.degree) (hnng : 0 P.leading_coeff) :
theorem polynomial.tendsto_at_bot_of_leading_coeff_nonpos {𝕜 : Type u_1} (P : polynomial 𝕜) (hdeg : 0 < P.degree) (hnps : P.leading_coeff 0) :
theorem polynomial.abs_tendsto_at_top {𝕜 : Type u_1} (P : polynomial 𝕜) (hdeg : 0 < P.degree) :
theorem polynomial.abs_is_bounded_under_iff {𝕜 : Type u_1} (P : polynomial 𝕜)  :
(λ (x : 𝕜), ||) P.degree 0
theorem polynomial.tendsto_nhds_iff {𝕜 : Type u_1} (P : polynomial 𝕜) {c : 𝕜} :
filter.tendsto (λ (x : 𝕜), P) filter.at_top (nhds c) P.degree 0
theorem polynomial.is_equivalent_at_top_div {𝕜 : Type u_1} (P Q : polynomial 𝕜)  :
(λ (x : 𝕜), / Q) (λ (x : 𝕜), * x ^ ((P.nat_degree) - (Q.nat_degree)))
theorem polynomial.div_tendsto_zero_of_degree_lt {𝕜 : Type u_1} (P Q : polynomial 𝕜) (hdeg : P.degree < Q.degree) :
filter.tendsto (λ (x : 𝕜), / Q) filter.at_top (nhds 0)
theorem polynomial.div_tendsto_zero_iff_degree_lt {𝕜 : Type u_1} (P Q : polynomial 𝕜) (hQ : Q 0) :
filter.tendsto (λ (x : 𝕜), / Q) filter.at_top (nhds 0) P.degree < Q.degree
theorem polynomial.div_tendsto_at_top_of_degree_gt' {𝕜 : Type u_1} (P Q : polynomial 𝕜) (hdeg : Q.degree < P.degree) (hpos : 0 < ) :
theorem polynomial.div_tendsto_at_top_of_degree_gt {𝕜 : Type u_1} (P Q : polynomial 𝕜) (hdeg : Q.degree < P.degree) (hQ : Q 0) (hnng : 0 ) :
theorem polynomial.div_tendsto_at_bot_of_degree_gt' {𝕜 : Type u_1} (P Q : polynomial 𝕜) (hdeg : Q.degree < P.degree) (hneg : < 0) :
theorem polynomial.div_tendsto_at_bot_of_degree_gt {𝕜 : Type u_1} (P Q : polynomial 𝕜) (hdeg : Q.degree < P.degree) (hQ : Q 0) (hnps : 0) :
theorem polynomial.abs_div_tendsto_at_top_of_degree_gt {𝕜 : Type u_1} (P Q : polynomial 𝕜) (hdeg : Q.degree < P.degree) (hQ : Q 0) :
theorem polynomial.is_O_of_degree_le {𝕜 : Type u_1} (P Q : polynomial 𝕜) (h : P.degree Q.degree) :
(λ (x : 𝕜), P) =O[filter.at_top] λ (x : 𝕜),