Documentation

Mathlib.Analysis.SpecialFunctions.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} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) (hP : P โ‰  0) :
โˆ€แถ  (x : ๐•œ) in Filter.atTop, ยฌP.IsRoot x
theorem Polynomial.isEquivalent_atTop_lead {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) [OrderTopology ๐•œ] :
Asymptotics.IsEquivalent Filter.atTop (fun (x : ๐•œ) => Polynomial.eval x P) fun (x : ๐•œ) => P.leadingCoeff * x ^ P.natDegree
theorem Polynomial.tendsto_atTop_of_leadingCoeff_nonneg {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) [OrderTopology ๐•œ] (hdeg : 0 < P.degree) (hnng : 0 โ‰ค P.leadingCoeff) :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P) Filter.atTop Filter.atTop
theorem Polynomial.tendsto_atTop_iff_leadingCoeff_nonneg {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) [OrderTopology ๐•œ] :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P) Filter.atTop Filter.atTop โ†” 0 < P.degree โˆง 0 โ‰ค P.leadingCoeff
theorem Polynomial.tendsto_atBot_iff_leadingCoeff_nonpos {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) [OrderTopology ๐•œ] :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P) Filter.atTop Filter.atBot โ†” 0 < P.degree โˆง P.leadingCoeff โ‰ค 0
theorem Polynomial.tendsto_atBot_of_leadingCoeff_nonpos {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) [OrderTopology ๐•œ] (hdeg : 0 < P.degree) (hnps : P.leadingCoeff โ‰ค 0) :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P) Filter.atTop Filter.atBot
theorem Polynomial.abs_tendsto_atTop {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) [OrderTopology ๐•œ] (hdeg : 0 < P.degree) :
Filter.Tendsto (fun (x : ๐•œ) => |Polynomial.eval x P|) Filter.atTop Filter.atTop
theorem Polynomial.abs_isBoundedUnder_iff {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) [OrderTopology ๐•œ] :
(Filter.IsBoundedUnder (fun (x x_1 : ๐•œ) => x โ‰ค x_1) Filter.atTop fun (x : ๐•œ) => |Polynomial.eval x P|) โ†” P.degree โ‰ค 0
theorem Polynomial.abs_tendsto_atTop_iff {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) [OrderTopology ๐•œ] :
Filter.Tendsto (fun (x : ๐•œ) => |Polynomial.eval x P|) Filter.atTop Filter.atTop โ†” 0 < P.degree
theorem Polynomial.tendsto_nhds_iff {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) [OrderTopology ๐•œ] {c : ๐•œ} :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P) Filter.atTop (nhds c) โ†” P.leadingCoeff = c โˆง P.degree โ‰ค 0
theorem Polynomial.isEquivalent_atTop_div {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) (Q : Polynomial ๐•œ) [OrderTopology ๐•œ] :
Asymptotics.IsEquivalent Filter.atTop (fun (x : ๐•œ) => Polynomial.eval x P / Polynomial.eval x Q) fun (x : ๐•œ) => P.leadingCoeff / Q.leadingCoeff * x ^ (โ†‘P.natDegree - โ†‘Q.natDegree)
theorem Polynomial.div_tendsto_zero_of_degree_lt {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) (Q : Polynomial ๐•œ) [OrderTopology ๐•œ] (hdeg : P.degree < Q.degree) :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop (nhds 0)
theorem Polynomial.div_tendsto_zero_iff_degree_lt {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) (Q : Polynomial ๐•œ) [OrderTopology ๐•œ] (hQ : Q โ‰  0) :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop (nhds 0) โ†” P.degree < Q.degree
theorem Polynomial.div_tendsto_leadingCoeff_div_of_degree_eq {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) (Q : Polynomial ๐•œ) [OrderTopology ๐•œ] (hdeg : P.degree = Q.degree) :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop (nhds (P.leadingCoeff / Q.leadingCoeff))
theorem Polynomial.div_tendsto_atTop_of_degree_gt' {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) (Q : Polynomial ๐•œ) [OrderTopology ๐•œ] (hdeg : Q.degree < P.degree) (hpos : 0 < P.leadingCoeff / Q.leadingCoeff) :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atTop
theorem Polynomial.div_tendsto_atTop_of_degree_gt {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) (Q : Polynomial ๐•œ) [OrderTopology ๐•œ] (hdeg : Q.degree < P.degree) (hQ : Q โ‰  0) (hnng : 0 โ‰ค P.leadingCoeff / Q.leadingCoeff) :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atTop
theorem Polynomial.div_tendsto_atBot_of_degree_gt' {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) (Q : Polynomial ๐•œ) [OrderTopology ๐•œ] (hdeg : Q.degree < P.degree) (hneg : P.leadingCoeff / Q.leadingCoeff < 0) :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atBot
theorem Polynomial.div_tendsto_atBot_of_degree_gt {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) (Q : Polynomial ๐•œ) [OrderTopology ๐•œ] (hdeg : Q.degree < P.degree) (hQ : Q โ‰  0) (hnps : P.leadingCoeff / Q.leadingCoeff โ‰ค 0) :
Filter.Tendsto (fun (x : ๐•œ) => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atBot
theorem Polynomial.abs_div_tendsto_atTop_of_degree_gt {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) (Q : Polynomial ๐•œ) [OrderTopology ๐•œ] (hdeg : Q.degree < P.degree) (hQ : Q โ‰  0) :
Filter.Tendsto (fun (x : ๐•œ) => |Polynomial.eval x P / Polynomial.eval x Q|) Filter.atTop Filter.atTop
theorem Polynomial.isBigO_of_degree_le {๐•œ : Type u_1} [NormedLinearOrderedField ๐•œ] (P : Polynomial ๐•œ) (Q : Polynomial ๐•œ) [OrderTopology ๐•œ] (h : P.degree โ‰ค Q.degree) :
(fun (x : ๐•œ) => Polynomial.eval x P) =O[Filter.atTop] fun (x : ๐•œ) => Polynomial.eval x Q