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 encoding of an iterated derivative is a restriction of the encoding of p, and strictly monotone ring embeddings preserve encodings. Negating or scaling p negates or scales its derivative signs, and an affine substitution X ↦ a X + b multiplies the sign of the kth derivative by sign a ^ k and moves the point to a x + b. 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.

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

theorem TauCeti.derivativeSign_eq_of_forall_le {R : Type u_1} [Semiring R] [LinearOrder R] {p : Polynomial R} {a b : R} {n d k : ℕ} (hd : p.natDegree ≤ d) (h : ∀ (j : ℕ), n ≤ j → j ≤ d → p.derivativeSign a j = p.derivativeSign b j) (hk : n ≤ k) : p.derivativeSign a k = p.derivativeSign b k

Agreement of derivative signs from order n through a degree bound extends to every order at least n, since higher derivatives vanish.

@[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.

theorem Polynomial.cons_zero_derivativeSign_succ_eq {R : Type u_1} [Semiring R] [LinearOrder R] {p : Polynomial R} (d : ℕ) {x : R} (hx : eval x p = 0) : (Fin.cons 0 fun (j : Fin d) => p.derivativeSign x (↑j + 1)) = fun (i : Fin (d + 1)) => p.derivativeSign x ↑i

Prepending 0 to the derivative signs of orders 1, …, d at a root gives the derivative signs of orders 0, …, d.

@[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.

@[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.thomEncoding_iterate_derivative_apply {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) (k : ℕ) (i : Fin ((⇑derivative)^[k] p).natDegree) : ((⇑derivative)^[k] p).thomEncoding x i = p.thomEncoding x ⟨↑i + k, ⋯⟩

Restriction to a derivative. Coordinate i of the Thom encoding of the kth derivative is coordinate i + k of the Thom encoding of p.

theorem Polynomial.thomEncoding_derivative_apply {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (x : R) (i : Fin (derivative p).natDegree) : (derivative p).thomEncoding x i = p.thomEncoding x ⟨↑i + 1, ⋯⟩

Coordinate i of the Thom encoding of p' is coordinate i + 1 of that of p.

theorem Polynomial.thomEncoding_eq_iff_iterate_derivative {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (a b : R) (k : ℕ) : p.thomEncoding a = p.thomEncoding b ↔ (∀ (j : ℕ), 0 < j → j ≤ k → p.derivativeSign a j = p.derivativeSign b j) ∧ ((⇑derivative)^[k] p).thomEncoding a = ((⇑derivative)^[k] p).thomEncoding b

Two points have the same Thom encoding for p exactly when the signs of the derivatives of orders 1, …, k agree and the Thom encodings for the kth derivative agree.

theorem Polynomial.thomEncoding_eq_iff_derivative {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) (a b : R) : p.thomEncoding a = p.thomEncoding b ↔ p.derivativeSign a 1 = p.derivativeSign b 1 ∧ (derivative p).thomEncoding a = (derivative p).thomEncoding b

Two points have the same Thom encoding for p exactly when p' has the same sign at both and they have the same Thom encoding for p'.

theorem TauCeti.sign_eval_map_iterate_derivative {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] [LinearOrder S] {p : Polynomial R} {f : R →+* S} (x : S) (k : ℕ) : SignType.sign (Polynomial.eval x (Polynomial.map f ((⇑Polynomial.derivative)^[k] p))) = (Polynomial.map f p).derivativeSign x k

Mapping an iterated derivative and taking its sign gives the derivative sign of the mapped polynomial.

@[simp]

theorem Polynomial.derivativeSign_map {R : Type u_1} [Semiring R] [LinearOrder R] {S : Type u_2} [Semiring S] [LinearOrder S] (p : Polynomial R) (f : R →+* S) (hf : StrictMono ⇑f) (x : R) (k : ℕ) : (map f p).derivativeSign (f x) k = p.derivativeSign x k

Strictly monotone ring embeddings preserve the signs of all derivatives.

theorem Polynomial.thomEncoding_map {R : Type u_1} [Semiring R] [LinearOrder R] {S : Type u_2} [Semiring S] [LinearOrder S] (p : Polynomial R) (f : R →+* S) (hf : StrictMono ⇑f) (x : R) : (map f p).thomEncoding (f x) = p.thomEncoding x ∘ Fin.cast ⋯

Strictly monotone ring embeddings preserve Thom encodings. The two encodings are words of the same length, since injective maps preserve the degree.

@[simp]

theorem Polynomial.derivativeSign_neg {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] (p : Polynomial R) (x : R) (k : ℕ) : (-p).derivativeSign x k = -p.derivativeSign x k

Negating the polynomial negates every derivative sign.

theorem Polynomial.thomEncoding_neg {R : Type u_1} [Ring R] [LinearOrder R] [IsOrderedRing R] (p : Polynomial R) (x : R) : (-p).thomEncoding x = -p.thomEncoding x ∘ Fin.cast ⋯

Negating the polynomial negates its Thom encoding.

@[simp]

theorem Polynomial.derivativeSign_C_mul {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (c : R) (p : Polynomial R) (x : R) (k : ℕ) : (C c * p).derivativeSign x k = SignType.sign c * p.derivativeSign x k

Scaling the polynomial by c multiplies every derivative sign by sign c.

theorem Polynomial.thomEncoding_C_mul {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {c : R} (hc : c ≠ 0) (p : Polynomial R) (x : R) : (C c * p).thomEncoding x = fun (i : Fin (C c * p).natDegree) => SignType.sign c * p.thomEncoding x (Fin.cast ⋯ i)

Scaling the polynomial by a nonzero c multiplies its Thom encoding by sign c.

@[simp]

theorem Polynomial.derivativeSign_comp_C_mul_X_add_C {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (a b x : R) (k : ℕ) : (p.comp (C a * X + C b)).derivativeSign x k = SignType.sign a ^ k * p.derivativeSign (a * x + b) k

Affine change of variable. The kth derivative sign of p (a X + b) at x is the kth derivative sign of p at a x + b, multiplied by sign a ^ k.

theorem Polynomial.thomEncoding_comp_C_mul_X_add_C {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} (ha : a ≠ 0) (b : R) (p : Polynomial R) (x : R) : (p.comp (C a * X + C b)).thomEncoding x = fun (i : Fin (p.comp (C a * X + C b)).natDegree) => SignType.sign a ^ (↑i + 1) * p.thomEncoding (a * x + b) (Fin.cast ⋯ i)

Affine change of variable. Coordinate i of the Thom encoding of p (a X + b) at x, for a ≠ 0, is coordinate i of the Thom encoding of p at a x + b, multiplied by sign a ^ (i + 1).

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.derivativeSign_ne_zero_of_derivativeSign_eq {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (hrolle : TauCeti.PolynomialRolle R) {a b : R} (hab : a ≠ b) (h : p.derivativeSign a = p.derivativeSign b) {k : ℕ} (hk : (⇑derivative)^[k] p ≠ 0) : p.derivativeSign a k ≠ 0

If all derivative signs of p agree at two distinct points, then every nonzero derivative of p has a nonzero sign there.

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.eq_of_derivativeSign_succ_eq_of_natDegree_le {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {p : Polynomial R} {d : ℕ} (hd : p.natDegree ≤ d) (hrolle : TauCeti.PolynomialRolle R) (hp : p ≠ 0) {a b : R} (ha : eval a p = 0) (hb : eval b p = 0) (h : (fun (j : Fin d) => p.derivativeSign a (↑j + 1)) = fun (j : Fin d) => p.derivativeSign b (↑j + 1)) : a = b

Roots of a nonzero polynomial with the same derivative signs of orders 1, …, d (where p.natDegree ≤ d) are equal.

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.

theorem Polynomial.derivativeSign_ne_of_eval_eq_zero {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {p : Polynomial R} {d : ℕ} (hd : p.natDegree ≤ d) (hrolle : TauCeti.PolynomialRolle R) (hp : p ≠ 0) {a b : R} (hab : a ≠ b) (hb : eval b p = 0) : (fun (i : Fin (d + 1)) => p.derivativeSign a ↑i) ≠ fun (i : Fin (d + 1)) => p.derivativeSign b ↑i

A root and a distinct point have different derivative signs through any degree bound.