Thom's lemma: sign conditions on all derivatives are open intervals

Over a real closed ordered field, fix signs for every formal derivative of a polynomial p, including p itself. The set of points realizing these signs is empty, a single point, or an open interval whose endpoints are points of the field or infinite (Polynomial.preimage_derivativeSign_subsingleton_or_eq_Ioo). The finite Thom sign conditions, on the derivatives of orders 1, …, natDegree p, have the same shape (Polynomial.preimage_thomEncoding_subsingleton_or_eq_Ioo).

Polynomial.ordConnected_preimage_derivativeSign already shows that these sets are order-convex. Over a non-Archimedean real closed field an order-convex set need not have endpoints in the field, so the existence of the endpoints is the additional content here: when the condition is realized at two points, the realizing set is a whole interval between consecutive roots of the nonzero derivatives. Its endpoints are such roots or infinite. Endpoints are written in WithBot R and WithTop R, so that ⊥ and ⊤ stand for the two infinities. No assumption on p is needed: the zero polynomial realizes only the zero condition, on the whole line.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Proposition 2.27 (Thom's lemma).

theorem Polynomial.derivativeSign_eq_of_forall_eval_ne_zero {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (h : ∀ z ∈ Set.uIcc a b, ∀ (k : ℕ), (⇑derivative)^[k] p ≠ 0 → eval z ((⇑derivative)^[k] p) ≠ 0) : p.derivativeSign a = p.derivativeSign b

If no nonzero derivative of p, of any order, has a root between a and b, then every derivative of p has the same sign at a as at b.

theorem Polynomial.preimage_derivativeSign_subsingleton_or_eq_Ioo {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) (σ : ℕ → SignType) : (p.derivativeSign ⁻¹' {σ}).Subsingleton ∨ ∃ (a : WithBot R) (b : WithTop R), p.derivativeSign ⁻¹' {σ} = {x : R | a < ↑x ∧ ↑x < b}

Thom's lemma. For any signs σ k prescribed for the derivatives of every order of p, including order zero, the set of points where p realizes them is empty, a single point, or an open interval with endpoints a ∈ WithBot R and b ∈ WithTop R.

theorem Polynomial.preimage_thomEncoding_subsingleton_or_eq_Ioo {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) (τ : Fin p.natDegree → SignType) : (p.thomEncoding ⁻¹' {τ}).Subsingleton ∨ ∃ (a : WithBot R) (b : WithTop R), p.thomEncoding ⁻¹' {τ} = {x : R | a < ↑x ∧ ↑x < b}

Thom's lemma for finite Thom encodings. For any signs τ prescribed for the derivatives of orders 1, …, natDegree p, the set of points where p realizes them is empty, a single point, or an open interval with endpoints a ∈ WithBot R and b ∈ WithTop R.