mathlib3 documentation

analysis.special_functions.polynomials

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) :

∀ᶠ (x : 𝕜) in filter.at_top , ¬P.is_root x

theorem polynomial.is_equivalent_at_top_lead {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P : polynomial 𝕜) [order_topology 𝕜] :

asymptotics.is_equivalent filter.at_top (λ (x : 𝕜), polynomial.eval x P) (λ (x : 𝕜), P.leading_coeff * x ^ P.nat_degree)

theorem polynomial.tendsto_at_top_of_leading_coeff_nonneg {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P : polynomial 𝕜) [order_topology 𝕜] (hdeg : 0 < P.degree) (hnng : 0 ≤ P.leading_coeff) :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P) filter.at_top filter.at_top

theorem polynomial.tendsto_at_top_iff_leading_coeff_nonneg {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P : polynomial 𝕜) [order_topology 𝕜] :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P) filter.at_top filter.at_top ↔ 0 < P.degree ∧ 0 ≤ P.leading_coeff

theorem polynomial.tendsto_at_bot_iff_leading_coeff_nonpos {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P : polynomial 𝕜) [order_topology 𝕜] :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P) filter.at_top filter.at_bot ↔ 0 < P.degree ∧ P.leading_coeff ≤ 0

theorem polynomial.tendsto_at_bot_of_leading_coeff_nonpos {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P : polynomial 𝕜) [order_topology 𝕜] (hdeg : 0 < P.degree) (hnps : P.leading_coeff ≤ 0) :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P) filter.at_top filter.at_bot

theorem polynomial.abs_tendsto_at_top {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P : polynomial 𝕜) [order_topology 𝕜] (hdeg : 0 < P.degree) :

filter.tendsto (λ (x : 𝕜), |polynomial.eval x P|) filter.at_top filter.at_top

theorem polynomial.abs_is_bounded_under_iff {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P : polynomial 𝕜) [order_topology 𝕜] :

filter.is_bounded_under has_le.le filter.at_top (λ (x : 𝕜), |polynomial.eval x P|) ↔ P.degree ≤ 0

theorem polynomial.abs_tendsto_at_top_iff {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P : polynomial 𝕜) [order_topology 𝕜] :

filter.tendsto (λ (x : 𝕜), |polynomial.eval x P|) filter.at_top filter.at_top ↔ 0 < P.degree

theorem polynomial.tendsto_nhds_iff {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P : polynomial 𝕜) [order_topology 𝕜] {c : 𝕜} :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P) filter.at_top (nhds c) ↔ P.leading_coeff = c ∧ P.degree ≤ 0

theorem polynomial.is_equivalent_at_top_div {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P Q : polynomial 𝕜) [order_topology 𝕜] :

asymptotics.is_equivalent filter.at_top (λ (x : 𝕜), polynomial.eval x P / polynomial.eval x Q) (λ (x : 𝕜), P.leading_coeff / Q.leading_coeff * x ^ (↑(P.nat_degree) - ↑(Q.nat_degree)))

theorem polynomial.div_tendsto_zero_of_degree_lt {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P Q : polynomial 𝕜) [order_topology 𝕜] (hdeg : P.degree < Q.degree) :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P / polynomial.eval x Q) filter.at_top (nhds 0)

theorem polynomial.div_tendsto_zero_iff_degree_lt {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P Q : polynomial 𝕜) [order_topology 𝕜] (hQ : Q ≠ 0) :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P / polynomial.eval x Q) filter.at_top (nhds 0) ↔ P.degree < Q.degree

theorem polynomial.div_tendsto_leading_coeff_div_of_degree_eq {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P Q : polynomial 𝕜) [order_topology 𝕜] (hdeg : P.degree = Q.degree) :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P / polynomial.eval x Q) filter.at_top (nhds (P.leading_coeff / Q.leading_coeff))

theorem polynomial.div_tendsto_at_top_of_degree_gt' {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P Q : polynomial 𝕜) [order_topology 𝕜] (hdeg : Q.degree < P.degree) (hpos : 0 < P.leading_coeff / Q.leading_coeff) :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P / polynomial.eval x Q) filter.at_top filter.at_top

theorem polynomial.div_tendsto_at_top_of_degree_gt {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P Q : polynomial 𝕜) [order_topology 𝕜] (hdeg : Q.degree < P.degree) (hQ : Q ≠ 0) (hnng : 0 ≤ P.leading_coeff / Q.leading_coeff) :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P / polynomial.eval x Q) filter.at_top filter.at_top

theorem polynomial.div_tendsto_at_bot_of_degree_gt' {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P Q : polynomial 𝕜) [order_topology 𝕜] (hdeg : Q.degree < P.degree) (hneg : P.leading_coeff / Q.leading_coeff < 0) :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P / polynomial.eval x Q) filter.at_top filter.at_bot

theorem polynomial.div_tendsto_at_bot_of_degree_gt {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P Q : polynomial 𝕜) [order_topology 𝕜] (hdeg : Q.degree < P.degree) (hQ : Q ≠ 0) (hnps : P.leading_coeff / Q.leading_coeff ≤ 0) :

filter.tendsto (λ (x : 𝕜), polynomial.eval x P / polynomial.eval x Q) filter.at_top filter.at_bot

theorem polynomial.abs_div_tendsto_at_top_of_degree_gt {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P Q : polynomial 𝕜) [order_topology 𝕜] (hdeg : Q.degree < P.degree) (hQ : Q ≠ 0) :

filter.tendsto (λ (x : 𝕜), |polynomial.eval x P / polynomial.eval x Q|) filter.at_top filter.at_top

theorem polynomial.is_O_of_degree_le {𝕜 : Type u_1} [normed_linear_ordered_field 𝕜] (P Q : polynomial 𝕜) [order_topology 𝕜] (h : P.degree ≤ Q.degree) :

(λ (x : 𝕜), polynomial.eval x P) =O[filter.at_top ] λ (x : 𝕜), polynomial.eval x Q