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