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.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