mathlib documentation

analysis.special_functions.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} [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 π•œ] :
(Ξ» (x : π•œ), polynomial.eval x P) ~[filter.at_top] Ξ» (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 : 1 ≀ P.degree) (hnng : 0 ≀ P.leading_coeff) :
theorem polynomial.tendsto_at_bot_of_leading_coeff_nonpos {π•œ : Type u_1} [normed_linear_ordered_field π•œ] (P : polynomial π•œ) [order_topology π•œ] (hdeg : 1 ≀ P.degree) (hnps : P.leading_coeff ≀ 0) :
theorem polynomial.abs_tendsto_at_top {π•œ : Type u_1} [normed_linear_ordered_field π•œ] (P : polynomial π•œ) [order_topology π•œ] (hdeg : 1 ≀ P.degree) :
theorem polynomial.abs_is_bounded_under_iff {π•œ : Type u_1} [normed_linear_ordered_field π•œ] (P : polynomial π•œ) [order_topology π•œ] :
theorem polynomial.abs_tendsto_at_top_iff {π•œ : Type u_1} [normed_linear_ordered_field π•œ] (P : polynomial π•œ) [order_topology π•œ] :
theorem polynomial.tendsto_nhds_iff {π•œ : Type u_1} [normed_linear_ordered_field π•œ] (P : polynomial π•œ) [order_topology π•œ] {c : π•œ} :
theorem polynomial.is_equivalent_at_top_div {π•œ : Type u_1} [normed_linear_ordered_field π•œ] (P Q : polynomial π•œ) [order_topology π•œ] :
(Ξ» (x : π•œ), polynomial.eval x P / polynomial.eval x Q) ~[filter.at_top] Ξ» (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) :
theorem polynomial.div_tendsto_zero_iff_degree_lt {π•œ : Type u_1} [normed_linear_ordered_field π•œ] (P Q : polynomial π•œ) [order_topology π•œ] (hQ : Q β‰  0) :
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) :
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) :
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) :
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) :
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) :
theorem polynomial.is_O_of_degree_le {π•œ : Type u_1} [normed_linear_ordered_field π•œ] (P Q : polynomial π•œ) [order_topology π•œ] (h : P.degree ≀ Q.degree) :
asymptotics.is_O (Ξ» (x : π•œ), polynomial.eval x P) (Ξ» (x : π•œ), polynomial.eval x Q) filter.at_top