Thom sign conditions from polynomial Rolle

Sign conditions on all formal derivatives are order-convex. Consequently a nonzero polynomial has no root between two distinct points at which all its derivatives have the same signs, and the signs of the positive-order derivatives distinguish roots of a nonzero polynomial, including multiple roots. No squarefreeness assumption is needed. The finite Thom encoding records derivatives 1 through natDegree. The last differing derivative sign and the next common sign determine the order of two points. The only extra premise on the ordered field is polynomial Rolle, supplied by TauCeti.RealClosure.polynomialRolle_of_isRealClosed over every real closed ordered field.

References

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

noncomputable def Polynomial.derivativeSign {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) (k : ℕ) : SignType

The sign of the kth formal derivative at x, including order zero.

Equations

• p.derivativeSign x k = SignType.sign (Polynomial.eval x ((⇑Polynomial.derivative)^[k] p))

theorem Polynomial.derivativeSign_def {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) (k : ℕ) : p.derivativeSign x k = SignType.sign (eval x ((⇑derivative)^[k] p))

Derivative signs are signs of evaluations of iterated formal derivatives.

theorem Polynomial.derivativeSign_eq_one_iff {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) (k : ℕ) : p.derivativeSign x k = 1 ↔ 0 < eval x ((⇑derivative)^[k] p)

theorem Polynomial.derivativeSign_eq_neg_one_iff {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) (k : ℕ) : p.derivativeSign x k = -1 ↔ eval x ((⇑derivative)^[k] p) < 0

@[simp]

theorem Polynomial.derivativeSign_eq_zero_iff {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) (k : ℕ) : p.derivativeSign x k = 0 ↔ eval x ((⇑derivative)^[k] p) = 0

theorem Polynomial.derivativeSign_ne_zero {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) (k : ℕ) : p.derivativeSign x k ≠ 0 ↔ eval x ((⇑derivative)^[k] p) ≠ 0

@[simp]

theorem Polynomial.derivativeSign_zero {R : Type u_1} [Semiring R] [LinearOrder R] (x : R) (k : ℕ) : derivativeSign 0 x k = 0

@[simp]

theorem Polynomial.derivativeSign_index_zero {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) : p.derivativeSign x 0 = SignType.sign (eval x p)

@[simp]

theorem Polynomial.derivativeSign_eq_zero {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) {k : ℕ} (hk : p.natDegree < k) : p.derivativeSign x k = 0

@[simp]

theorem Polynomial.derivativeSign_C {R : Type u_1} [Semiring R] [LinearOrder R] (a x : R) (k : ℕ) : (C a).derivativeSign x k = if k = 0 then SignType.sign a else 0

@[simp]

theorem Polynomial.derivativeSign_derivative {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) (k : ℕ) : (derivative p).derivativeSign x k = p.derivativeSign x (k + 1)

Taking one derivative advances the derivative-sign index by one.

@[simp]

theorem Polynomial.derivativeSign_iterate_derivative {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) (i j : ℕ) : ((⇑derivative)^[i] p).derivativeSign x j = p.derivativeSign x (j + i)

Shifting the polynomial shifts the derivative index.

noncomputable def Polynomial.thomEncoding {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) : Fin p.natDegree → SignType

The usual finite Thom encoding retains derivatives 1 through the degree.

Equations

• p.thomEncoding x i = p.derivativeSign x (↑i + 1)

@[simp]

theorem Polynomial.thomEncoding_apply {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) (i : Fin p.natDegree) : p.thomEncoding x i = p.derivativeSign x (↑i + 1)

Coordinate i records the sign of derivative i + 1.

theorem Polynomial.thomEncoding_def {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) : p.thomEncoding x = fun (i : Fin p.natDegree) => SignType.sign (eval x ((⇑derivative)^[↑i + 1] p))

A finite Thom word consists of the signs of derivatives 1 through the degree.

theorem Polynomial.thomEncoding_eq_iff {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (a b : R) : p.thomEncoding a = p.thomEncoding b ↔ ∀ (k : ℕ), 0 < k → p.derivativeSign a k = p.derivativeSign b k

Finite Thom encodings agree exactly when all positive-order derivative signs agree.

theorem Polynomial.derivativeSign_const {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (a b : R) {k : ℕ} (hk : p.natDegree ≤ k) : p.derivativeSign a k = p.derivativeSign b k

At and above the degree the derivative is constant, so its sign is independent of the point.

theorem Polynomial.thomEncoding_succ_lt_natDegree {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) {a b : R} {i : Fin p.natDegree} (hne : p.thomEncoding a i ≠ p.thomEncoding b i) : ↑i + 1 < p.natDegree

A differing finite Thom coordinate lies below the top derivative, so a next coordinate exists.

theorem Polynomial.exists_derivativeSign_ne {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) {a b : R} (henc : p.thomEncoding a ≠ p.thomEncoding b) : ∃ (k : ℕ), 0 < k ∧ k < p.natDegree ∧ p.derivativeSign a k ≠ p.derivativeSign b k ∧ ∀ (j : ℕ), k < j → p.derivativeSign a j = p.derivativeSign b j

Distinct Thom encodings have a last disagreement strictly below the degree. All larger derivative signs agree, including the highest derivative sign. For distinct roots, thomEncoding_injOn supplies the unequal encodings.

theorem Polynomial.exists_thomEncoding_ne {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) {a b : R} (henc : p.thomEncoding a ≠ p.thomEncoding b) : ∃ (i : Fin p.natDegree), p.thomEncoding a i ≠ p.thomEncoding b i ∧ ∀ (j : Fin p.natDegree), i < j → p.thomEncoding a j = p.thomEncoding b j

Distinct finite Thom encodings have a last differing coordinate.

theorem Polynomial.derivativeSign_eq_on_Icc {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hrolle : TauCeti.PolynomialRolle R) {a b x : R} (hx : x ∈ Set.Icc a b) {k : ℕ} (h : ∀ (j : ℕ), k ≤ j → p.derivativeSign a j = p.derivativeSign b j) : p.derivativeSign x k = p.derivativeSign a k

Agreement of all derivative signs from index k onward forces the sign at index k to be constant between the endpoints.

theorem Polynomial.ordConnected_preimage_derivativeSign {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hrolle : TauCeti.PolynomialRolle R) (σ : ℕ → SignType) : (p.derivativeSign ⁻¹' {σ}).OrdConnected

A full derivative sign condition is order-convex. Empty conditions are allowed; this statement does not assert that an arbitrary word is realizable.

theorem Polynomial.ordConnected_preimage_thomEncoding {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hrolle : TauCeti.PolynomialRolle R) (τ : Fin p.natDegree → SignType) : (p.thomEncoding ⁻¹' {τ}).OrdConnected

A finite Thom sign condition is order-convex, including unrealized conditions.

theorem Polynomial.eval_ne_zero_of_derivativeSign_eq {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hrolle : TauCeti.PolynomialRolle R) (hp : p ≠ 0) {a b x : R} (hab : a ≠ b) (h : ∀ (k : ℕ), p.derivativeSign a k = p.derivativeSign b k) (hx : x ∈ Set.uIcc a b) : eval x p ≠ 0

A nonzero polynomial whose derivatives of every order, including order zero, have the same signs at two distinct points has no root between them.

theorem Polynomial.eq_of_derivativeSign_eq {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hrolle : TauCeti.PolynomialRolle R) (hp : p ≠ 0) {a b : R} (ha : eval a p = 0) (hb : eval b p = 0) (hs : ∀ (k : ℕ), 0 < k → p.derivativeSign a k = p.derivativeSign b k) : a = b

Roots with equal signs of every positive-order derivative are equal. The polynomial need not be squarefree.

theorem Polynomial.thomEncoding_injOn {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hrolle : TauCeti.PolynomialRolle R) (hp : p ≠ 0) : Set.InjOn p.thomEncoding {x : R | eval x p = 0}

A finite Thom encoding uniquely identifies a root of a nonzero polynomial.

theorem Polynomial.lt_iff_derivativeSign {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hrolle : TauCeti.PolynomialRolle R) {a b : R} {k : ℕ} (hne : p.derivativeSign a k ≠ p.derivativeSign b k) (htail : ∀ (j : ℕ), k < j → p.derivativeSign a j = p.derivativeSign b j) : a < b ↔ p.derivativeSign a (k + 1) = 1 ∧ p.derivativeSign a k < p.derivativeSign b k ∨ p.derivativeSign a (k + 1) = -1 ∧ p.derivativeSign b k < p.derivativeSign a k

At the largest derivative index where signs differ, the next common sign and the two differing signs determine the order of the points.

theorem Polynomial.lt_iff_thomEncoding {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hrolle : TauCeti.PolynomialRolle R) {a b : R} (i : Fin p.natDegree) (hne : p.thomEncoding a i ≠ p.thomEncoding b i) (htail : ∀ (j : Fin p.natDegree), i < j → p.thomEncoding a j = p.thomEncoding b j) : a < b ↔ p.thomEncoding a ⟨↑i + 1, ⋯⟩ = 1 ∧ p.thomEncoding a i < p.thomEncoding b i ∨ p.thomEncoding a ⟨↑i + 1, ⋯⟩ = -1 ∧ p.thomEncoding b i < p.thomEncoding a i

The comparison rule directly on finite Thom words. thomEncoding_succ_lt_natDegree supplies existence of the next coordinate from the differing signs. Every coordinate above the disagreement must agree.

theorem Polynomial.derivativeSign_succ_ne_zero {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hrolle : TauCeti.PolynomialRolle R) {a b : R} {k : ℕ} (hne : p.derivativeSign a k ≠ p.derivativeSign b k) (htail : ∀ (j : ℕ), k < j → p.derivativeSign a j = p.derivativeSign b j) : p.derivativeSign a (k + 1) ≠ 0

The common sign immediately above the last disagreement cannot be zero.

theorem Polynomial.thomEncoding_succ_ne_zero {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hrolle : TauCeti.PolynomialRolle R) {a b : R} (i : Fin p.natDegree) (hne : p.thomEncoding a i ≠ p.thomEncoding b i) (htail : ∀ (j : Fin p.natDegree), i < j → p.thomEncoding a j = p.thomEncoding b j) : p.thomEncoding a ⟨↑i + 1, ⋯⟩ ≠ 0

The common finite Thom coordinate immediately above the last disagreement is nonzero.