The signs of a polynomial near a point and near infinity

Candidates for Mathlib.Analysis.Polynomial.Order: over a linearly ordered normed field with the order topology, such as ℝ, a nonzero polynomial has, far right, the sign of its leading coefficient and, far left, that sign times (-1) ^ deg (Polynomial.eventually_atTop_sign_eval, Polynomial.eventually_atBot_sign_eval); near a point it keeps a nonzero sign (Polynomial.eventually_sign_eval_eq), near a root x where its derivative does not vanish it has the sign of (y - x) p'(x) at y (Polynomial.eventually_sign_eval_eq_sign_sub_mul), and just right of a point x where it or its derivative does not vanish it has the sign of p(x), or of p'(x) when p(x) = 0, and just left of x that of p(x), or of -p'(x) when p(x) = 0 (Polynomial.eventually_sign_eval_nhdsGT, Polynomial.eventually_sign_eval_nhdsLT). By the intermediate value theorem, opposite signs of a real polynomial at two points give a root between them (Polynomial.exists_isRoot_of_eval_mul_eval_neg), a negative sign just right of the left end of an interval without a root holds on the whole interval (Polynomial.eval_neg_of_forall_not_isRoot), and a nonzero real polynomial of degree n changes its sign at most n times along increasing points (Polynomial.length_le_natDegree_add_one_of_isChain).

Implementation notes

The file imports its sibling Mathlib.Analysis.Polynomial.Order, the sibling's private import Mathlib.Topology.Algebra.Polynomial for the continuity of polynomials, and, publicly, Mathlib.Algebra.Polynomial.Derivative, which the statements just right and just left of a point name and the sibling's public imports lack.

The lemmas that rest on the intermediate value theorem are stated over ℝ, as the sibling's are: they need a conditionally complete, densely ordered field.

The signs just right and just left of a point are stated by the case distinction on p(x) = 0, without a definition of their own; compare Polynomial.signRight of Mathlib pull request #44248, the sign just right of a point as a limit, for every p.

theorem Polynomial.eventually_sign_eval_eq {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [OrderTopology 𝕜] {p : Polynomial 𝕜} {x : 𝕜} (h : eval x p ≠ 0) : ∀ᶠ (y : 𝕜) in nhds x, SignType.sign (eval y p) = SignType.sign (eval x p)

Near a point where it does not vanish, a polynomial keeps its sign.

theorem Polynomial.eventually_atTop_sign_eval {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [OrderTopology 𝕜] [IsStrictOrderedRing 𝕜] {p : Polynomial 𝕜} (hp : p ≠ 0) : ∀ᶠ (x : 𝕜) in Filter.atTop, SignType.sign (eval x p) = SignType.sign p.leadingCoeff

Far right, a nonzero polynomial has the sign of its leading coefficient.

theorem Polynomial.eventually_atBot_sign_eval {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [OrderTopology 𝕜] [IsStrictOrderedRing 𝕜] {p : Polynomial 𝕜} (hp : p ≠ 0) : ∀ᶠ (x : 𝕜) in Filter.atBot, SignType.sign (eval x p) = SignType.sign ((-1) ^ p.natDegree * p.leadingCoeff)

Far left, a nonzero polynomial has the sign of (-1) ^ deg times its leading coefficient.

theorem Polynomial.eventually_sign_eval_eq_sign_sub_mul {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [OrderTopology 𝕜] [IsStrictOrderedRing 𝕜] {p : Polynomial 𝕜} {x : 𝕜} (h0 : eval x p = 0) (h : eval x (derivative p) ≠ 0) : ∀ᶠ (y : 𝕜) in nhds x, SignType.sign (eval y p) = SignType.sign (y - x) * SignType.sign (eval x (derivative p))

Near a root x of p with p'(x) ≠ 0, p(y) has the sign of (y - x) p'(x).

theorem Polynomial.eventually_sign_eval_nhdsGT {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [OrderTopology 𝕜] [IsStrictOrderedRing 𝕜] {p : Polynomial 𝕜} {x : 𝕜} (h : eval x p ≠ 0 ∨ eval x (derivative p) ≠ 0) : ∀ᶠ (y : 𝕜) in nhdsWithin x (Set.Ioi x), SignType.sign (eval y p) = if eval x p = 0 then SignType.sign (eval x (derivative p)) else SignType.sign (eval x p)

Just right of a point x where p(x) ≠ 0 or p'(x) ≠ 0, a polynomial p has the sign of p(x), or of p'(x) when p(x) = 0.

theorem Polynomial.eventually_sign_eval_nhdsLT {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [OrderTopology 𝕜] [IsStrictOrderedRing 𝕜] {p : Polynomial 𝕜} {x : 𝕜} (h : eval x p ≠ 0 ∨ eval x (derivative p) ≠ 0) : ∀ᶠ (y : 𝕜) in nhdsWithin x (Set.Iio x), SignType.sign (eval y p) = if eval x p = 0 then -SignType.sign (eval x (derivative p)) else SignType.sign (eval x p)

Just left of a point x where p(x) ≠ 0 or p'(x) ≠ 0, a polynomial p has the sign of p(x), or of -p'(x) when p(x) = 0.

theorem Polynomial.exists_isRoot_of_eval_mul_eval_neg {p : Polynomial ℝ} {a b : ℝ} (hab : a < b) (h : eval a p * eval b p < 0) : ∃ z ∈ Set.Ioo a b, p.IsRoot z

A real polynomial with values of opposite signs at a < b has a root strictly between.

theorem Polynomial.eval_neg_of_forall_not_isRoot {p : Polynomial ℝ} {l r : ℝ} (hroot : ∀ (x : ℝ), l < x → x < r → ¬p.IsRoot x) (hneg : ∀ᶠ (y : ℝ) in nhdsWithin l (Set.Ioi l), eval y p < 0) {x : ℝ} (hlx : l < x) (hxr : x < r) : eval x p < 0

An interval (l, r) without a root of a real polynomial p, on which p is negative just right of l, holds no x with p(x) ≥ 0.

theorem Polynomial.length_le_natDegree_add_one_of_isChain {p : Polynomial ℝ} (hp : p ≠ 0) {l : List ℝ} (hl : List.IsChain (fun (a b : ℝ) => a < b ∧ eval a p * eval b p < 0) l) : l.length ≤ p.natDegree + 1

A nonzero real polynomial p of degree n changes its sign at most n times along a strictly increasing list of points.