The Cauchy index of a quotient of polynomials

Polynomial.cauchyJump p q a is the jump of the rational function q / p at a. It is zero unless a is a pole of q / p of odd order. At such a pole it is +1 for a jump from -∞ to +∞ and -1 for a jump from +∞ to -∞. The sign of q / p immediately to the right of a is the right-hand sign of p * q, so the jump is defined algebraically from root multiplicities and Polynomial.signRight. It needs no topology and makes sense over any ordered field.

Polynomial.cauchyIndex p q s sums these jumps over a set s. Only roots of p contribute, so the sum is finite. As for Polynomial.tarskiQuery p q, the first argument supplies the denominator, and hence the roots. With this convention the index of p' / p counts distinct roots, and the index of p' * q / p on the whole line is the Tarski query TaQ(q, p).

The index depends only on the rational function q / p: cancelling a common factor does not change it, and neither does reducing q modulo p. Over a real closed field, if a < b and neither a nor b is a root of p * q, the indices of q / p and p / q on (a, b) sum to half the change of sign of p * q from a to b. With the reduction modulo p this gives the Euclidean recurrence for the index, under the same endpoint hypotheses.

Main declarations

• Polynomial.cauchyJump: the jump of q / p at a point.
• Polynomial.cauchyIndex: the sum of the jumps of q / p over a set.
• Polynomial.cauchyIndex_mul_right: cancellation of a common factor.
• Polynomial.cauchyIndex_mod: reduction of the numerator modulo the denominator.
• Polynomial.cauchyIndex_derivative: the index of p' / p counts distinct roots.
• Polynomial.cauchyIndex_derivative_mul_univ: the whole-line index of p' * q / p is tarskiQuery p q.
• Polynomial.two_mul_cauchyIndex_add_cauchyIndex_Ioo: the inversion formula on an interval (a, b) with a < b whose endpoints are not roots of p * q.
• Polynomial.two_mul_cauchyIndex_Ioo: the Euclidean recurrence, under the same hypotheses.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, §2.2.2 (the Cauchy index and its properties).

noncomputable def Polynomial.cauchyJump {R : Type u_1} [CommRing R] [LinearOrder R] (p q : Polynomial R) (a : R) : ℤ

The jump of q / p at a. It is the right-hand sign of p * q at a when a is a pole of q / p of odd order, and zero otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem Polynomial.cauchyJump_def {R : Type u_1} [CommRing R] [LinearOrder R] (p q : Polynomial R) (a : R) : p.cauchyJump q a = if rootMultiplicity a q < rootMultiplicity a p ∧ Odd (rootMultiplicity a p - rootMultiplicity a q) then ↑((p * q).signRight a) else 0

theorem Polynomial.cauchyJump_of_rootMultiplicity_le {R : Type u_1} [CommRing R] [LinearOrder R] {p q : Polynomial R} {a : R} (h : rootMultiplicity a p ≤ rootMultiplicity a q) : p.cauchyJump q a = 0

The jump vanishes where q / p has no pole.

theorem Polynomial.cauchyJump_of_eval_ne_zero {R : Type u_1} [CommRing R] [LinearOrder R] {p : Polynomial R} (q : Polynomial R) {a : R} (ha : eval a p ≠ 0) : p.cauchyJump q a = 0

The jump vanishes away from the roots of p.

@[simp]

theorem Polynomial.cauchyJump_zero_left {R : Type u_1} [CommRing R] [LinearOrder R] (q : Polynomial R) (a : R) : cauchyJump 0 q a = 0

@[simp]

theorem Polynomial.cauchyJump_zero_right {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) (a : R) : p.cauchyJump 0 a = 0

@[simp]

theorem Polynomial.cauchyJump_C {R : Type u_1} [CommRing R] [LinearOrder R] (c : R) (q : Polynomial R) (a : R) : (C c).cauchyJump q a = 0

A constant denominator has no poles.

noncomputable def Polynomial.cauchyIndex {R : Type u_1} [CommRing R] [LinearOrder R] (p q : Polynomial R) (s : Set R) : ℤ

The Cauchy index of q / p on s: the sum of the jumps of q / p at the points of s.

Equations

• p.cauchyIndex q s = ∑ᶠ (x : R) (_ : x ∈ s), p.cauchyJump q x

theorem Polynomial.cauchyIndex_def {R : Type u_1} [CommRing R] [LinearOrder R] (p q : Polynomial R) (s : Set R) : p.cauchyIndex q s = ∑ᶠ (x : R) (_ : x ∈ s), p.cauchyJump q x

@[simp]

theorem Polynomial.cauchyIndex_empty {R : Type u_1} [CommRing R] [LinearOrder R] (p q : Polynomial R) : p.cauchyIndex q ∅ = 0

@[simp]

theorem Polynomial.cauchyIndex_singleton {R : Type u_1} [CommRing R] [LinearOrder R] (p q : Polynomial R) (a : R) : p.cauchyIndex q {a} = p.cauchyJump q a

@[simp]

theorem Polynomial.cauchyIndex_zero_left {R : Type u_1} [CommRing R] [LinearOrder R] (q : Polynomial R) (s : Set R) : cauchyIndex 0 q s = 0

@[simp]

theorem Polynomial.cauchyIndex_zero_right {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) (s : Set R) : p.cauchyIndex 0 s = 0

@[simp]

theorem Polynomial.cauchyIndex_C {R : Type u_1} [CommRing R] [LinearOrder R] (c : R) (q : Polynomial R) (s : Set R) : (C c).cauchyIndex q s = 0

theorem Polynomial.support_cauchyJump_subset {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) : Function.support (p.cauchyJump q) ⊆ ↑p.roots.toFinset

Only roots of p carry a jump of q / p.

theorem Polynomial.finite_support_cauchyJump {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) : (Function.support (p.cauchyJump q)).Finite

Only finitely many points carry a jump of q / p.

@[simp]

theorem Polynomial.cauchyJump_neg_right {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) (a : R) : p.cauchyJump (-q) a = -p.cauchyJump q a

Negating the numerator reverses every Cauchy jump.

@[simp]

theorem Polynomial.cauchyIndex_neg_right {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) (s : Set R) : p.cauchyIndex (-q) s = -p.cauchyIndex q s

Negating the numerator reverses the Cauchy index on any set.

theorem Polynomial.cauchyIndex_eq_sum {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) (s : Set R) [DecidablePred fun (x : R) => x ∈ s] : p.cauchyIndex q s = ∑ x ∈ p.roots.toFinset with x ∈ s, p.cauchyJump q x

The Cauchy index as a finite sum over the distinct roots of p in s.

theorem Polynomial.cauchyIndex_union {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) {s t : Set R} (h : Disjoint s t) : p.cauchyIndex q (s ∪ t) = p.cauchyIndex q s + p.cauchyIndex q t

The Cauchy index is additive over disjoint sets.

theorem Polynomial.cauchyIndex_Ioo_eq_add {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {p q : Polynomial R} {a b c : R} (hab : a < b) (hbc : b < c) : p.cauchyIndex q (Set.Ioo a c) = p.cauchyIndex q (Set.Ioo a b) + p.cauchyJump q b + p.cauchyIndex q (Set.Ioo b c)

Splitting an open interval at an interior point adds the jump at that point.

theorem Polynomial.cauchyJump_mul_right {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) {r : Polynomial R} (hr : r ≠ 0) (a : R) : (p * r).cauchyJump (q * r) a = p.cauchyJump q a

Cancelling a common nonzero factor of p and q does not change the jumps of q / p.

theorem Polynomial.cauchyIndex_mul_right {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) {r : Polynomial R} (hr : r ≠ 0) (s : Set R) : (p * r).cauchyIndex (q * r) s = p.cauchyIndex q s

Cancelling a common nonzero factor of p and q does not change the index of q / p.

theorem Polynomial.cauchyJump_add_mul {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q r : Polynomial R) (a : R) : p.cauchyJump (q + p * r) a = p.cauchyJump q a

Adding a multiple of p to q does not change the jumps of q / p.

theorem Polynomial.cauchyIndex_add_mul {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q r : Polynomial R) (s : Set R) : p.cauchyIndex (q + p * r) s = p.cauchyIndex q s

Adding a multiple of p to q does not change the index of q / p.

theorem Polynomial.two_mul_cauchyJump_add_cauchyJump {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) (a : R) : 2 * (p.cauchyJump q a + q.cauchyJump p a) = ↑((p * q).signRight a) - ↑((p * q).signLeft a)

The jumps of q / p and of p / q at a point add up to half the jump of the one-sided signs of p * q there.

theorem Polynomial.cauchyJump_derivative_mul {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {p : Polynomial R} (hp : p ≠ 0) (q : Polynomial R) {a : R} (ha : eval a p = 0) : p.cauchyJump (derivative p * q) a = ↑(SignType.sign (eval a q))

At a root of a nonzero p, the jump of p' * q / p is the sign of q.

theorem Polynomial.cauchyIndex_derivative_mul {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) (s : Set R) [DecidablePred fun (x : R) => x ∈ s] : p.cauchyIndex (derivative p * q) s = ∑ x ∈ p.roots.toFinset with x ∈ s, ↑(SignType.sign (eval x q))

The index of p' * q / p on s is the sum of the signs of q at the distinct roots of p in s.

theorem Polynomial.cauchyIndex_derivative_mul_univ {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) : p.cauchyIndex (derivative p * q) Set.univ = p.tarskiQuery q

The whole-line index of p' * q / p is the Tarski query of q at the roots of p.

theorem Polynomial.cauchyIndex_derivative {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (p : Polynomial R) (s : Set R) [DecidablePred fun (x : R) => x ∈ s] : p.cauchyIndex (derivative p) s = ↑{x ∈ p.roots.toFinset | x ∈ s}.card

The index of p' / p on s is the number of distinct roots of p in s.

theorem Polynomial.cauchyJump_mod {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) (a : R) : p.cauchyJump (q % p) a = p.cauchyJump q a

Reducing q modulo p does not change the jumps of q / p.

theorem Polynomial.cauchyIndex_mod {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) (s : Set R) : p.cauchyIndex (q % p) s = p.cauchyIndex q s

Reducing q modulo p does not change the index of q / p.

theorem Polynomial.two_mul_cauchyIndex_add_cauchyIndex_Ioo {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p q : Polynomial R} {a b : R} (hab : a < b) (ha : eval a (p * q) ≠ 0) (hb : eval b (p * q) ≠ 0) : 2 * (p.cauchyIndex q (Set.Ioo a b) + q.cauchyIndex p (Set.Ioo a b)) = ↑(SignType.sign (eval b (p * q))) - ↑(SignType.sign (eval a (p * q)))

The inversion formula. On an interval whose endpoints are not roots of p * q, the indices of q / p and p / q add up to half the change of sign of p * q.

theorem Polynomial.two_mul_cauchyIndex_Ioo {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p q : Polynomial R} {a b : R} (hab : a < b) (ha : eval a (p * q) ≠ 0) (hb : eval b (p * q) ≠ 0) : 2 * p.cauchyIndex q (Set.Ioo a b) = ↑(SignType.sign (eval b (p * q))) - ↑(SignType.sign (eval a (p * q))) - 2 * q.cauchyIndex (p % q) (Set.Ioo a b)

The Euclidean recurrence for the Cauchy index. On an interval whose endpoints are not roots of p * q, the index of q / p is determined by the change of sign of p * q and the index of (p % q) / q.