mathlib3 documentation


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} [normed_linear_ordered_field 𝕜] (P : polynomial 𝕜) (hP : P 0) :
theorem polynomial.tendsto_nhds_iff {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P : polynomial 𝕜) [order_topology 𝕜] {c : 𝕜} :
theorem polynomial.is_O_of_degree_le {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P Q : polynomial 𝕜) [order_topology 𝕜] (h : :
(λ (x : 𝕜), polynomial.eval x P) =O[filter.at_top] λ (x : 𝕜), polynomial.eval x Q