Exact scaling along the signed remainder sequence

The structure theorem identifies subresultants with signed remainders up to nonzero scalars. Here Polynomial.sturmSubresultantFactor records the scalars explicitly as products of signs and powers of leading coefficients. For consecutive entries a, b, c of the signed remainder sequence, one reduction contributes (-1) ^ ((deg a - j + 1) * (deg b - j)) * lc(b) ^ (deg a - deg c). The first step uses a supplied formal bound m ≥ deg p in place of deg p. Multiplying these factors transports every subresultant below the next remainder degree.

Polynomial.subresultant_eq_sturmSubresultantFactor_mul gives this exact transport. The two endpoint formulas give the precise multiples of a remainder at the upper and lower ends of its degree gap. These identities retain the determinant normalization, rather than normalizing every remainder to be monic. They work in arbitrary characteristic, including two.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 8 (subresultants and signed remainder sequences).

noncomputable def Polynomial.sturmSubresultantFactor {K : Type u_1} [Field K] [DecidableEq K] (p q : Polynomial K) (m j i : ℕ) : K

The product of the first i Euclidean scaling factors for the subresultant of index j. The first step uses the formal left bound m; later steps use actual degrees. Missing entries of the signed remainder sequence are read as zero. The transport theorem uses this product only while the required entries exist and j is below the next entry's degree.

theorem Polynomial.sturmSubresultantFactor_def {K : Type u_1} [Field K] [DecidableEq K] (p q : Polynomial K) (m j i : ℕ) : p.sturmSubresultantFactor q m j i = ∏ k ∈ Finset.range i, (-1) ^ (((if k = 0 then m else ((p.sturmSeq q)[k]?.getD 0).natDegree) - j + 1) * (((p.sturmSeq q)[k + 1]?.getD 0).natDegree - j)) * ((p.sturmSeq q)[k + 1]?.getD 0).leadingCoeff ^ ((if k = 0 then m else ((p.sturmSeq q)[k]?.getD 0).natDegree) - ((p.sturmSeq q)[k + 2]?.getD 0).natDegree)

The scaling factor is the indicated finite product of signs and leading-coefficient powers.

@[simp]

theorem Polynomial.sturmSubresultantFactor_zero {K : Type u_1} [Field K] [DecidableEq K] (p q : Polynomial K) (m j : ℕ) : p.sturmSubresultantFactor q m j 0 = 1

@[simp]

theorem Polynomial.sturmSubresultantFactor_succ {K : Type u_1} [Field K] [DecidableEq K] (p q : Polynomial K) (m j i : ℕ) : p.sturmSubresultantFactor q m j (i + 1) = p.sturmSubresultantFactor q m j i * ((-1) ^ (((if i = 0 then m else ((p.sturmSeq q)[i]?.getD 0).natDegree) - j + 1) * (((p.sturmSeq q)[i + 1]?.getD 0).natDegree - j)) * ((p.sturmSeq q)[i + 1]?.getD 0).leadingCoeff ^ ((if i = 0 then m else ((p.sturmSeq q)[i]?.getD 0).natDegree) - ((p.sturmSeq q)[i + 2]?.getD 0).natDegree))

Extending the prefix multiplies its factor by the factor of the next Euclidean step.

theorem Polynomial.sturmSubresultantFactor_ne_zero {K : Type u_1} [Field K] [DecidableEq K] {p q a : Polynomial K} {i : ℕ} (ha : (p.sturmSeq q)[i]? = some a) (m j : ℕ) : p.sturmSubresultantFactor q m j i ≠ 0

All scaling factors are nonzero as long as the prefix ends at an actual sequence entry.

theorem Polynomial.natDegree_le_ite_of_getElem?_sturmSeq {K : Type u_1} [Field K] [DecidableEq K] {p q a : Polynomial K} {m i : ℕ} (hp : p.natDegree ≤ m) (ha : (p.sturmSeq q)[i]? = some a) : a.natDegree ≤ if i = 0 then m else a.natDegree

Each sequence entry satisfies the formal left bound used for its Euclidean step.

theorem Polynomial.subresultant_eq_sturmSubresultantFactor_mul {K : Type u_1} [Field K] [DecidableEq K] {p q a b : Polynomial K} {m i j : ℕ} (hp : p.natDegree ≤ m) (ha : (p.sturmSeq q)[i]? = some a) (hb : (p.sturmSeq q)[i + 1]? = some b) (hj : j < b.natDegree) : p.subresultant q m q.natDegree j = C (p.sturmSubresultantFactor q m j i) * a.subresultant b (if i = 0 then m else a.natDegree) b.natDegree j

Exact transport of subresultants along signed remainders. For the consecutive entries a, b at positions i, i + 1, every subresultant below deg b is the corresponding subresultant of (a, b) multiplied by the explicit product of the preceding step factors. The first left bound is m; subsequent left bounds are actual degrees. The first two input degrees need not be ordered.

theorem Polynomial.subresultant_natDegree_sub_one_eq_sturmSubresultantFactor_mul {K : Type u_1} [Field K] [DecidableEq K] {p q a b c : Polynomial K} {m i : ℕ} (hp : p.natDegree ≤ m) (hq : i = 0 → q.natDegree ≤ m) (ha : (p.sturmSeq q)[i]? = some a) (hb : (p.sturmSeq q)[i + 1]? = some b) (hc : (p.sturmSeq q)[i + 2]? = some c) : p.subresultant q m q.natDegree (b.natDegree - 1) = C (-(p.sturmSubresultantFactor q m (b.natDegree - 1) i * (-b.leadingCoeff) ^ ((if i = 0 then m else a.natDegree) + 1 - b.natDegree))) * c

The upper end of a degree gap, with its exact scalar. If a, b, c are consecutive signed remainders, the subresultant at deg b - 1 is the displayed nonzero scalar multiple of c. Only the initial pair additionally requires deg q ≤ m.

theorem Polynomial.subresultant_natDegree_eq_sturmSubresultantFactor_mul {K : Type u_1} [Field K] [DecidableEq K] {p q a b c : Polynomial K} {m i : ℕ} (hp : p.natDegree ≤ m) (hq : i = 0 → q.natDegree ≤ m) (ha : (p.sturmSeq q)[i]? = some a) (hb : (p.sturmSeq q)[i + 1]? = some b) (hc : (p.sturmSeq q)[i + 2]? = some c) : p.subresultant q m q.natDegree c.natDegree = C (-(p.sturmSubresultantFactor q m c.natDegree i * ((-1) ^ (((if i = 0 then m else a.natDegree) - c.natDegree) * (b.natDegree - c.natDegree)) * b.leadingCoeff ^ ((if i = 0 then m else a.natDegree) - c.natDegree) * (-c.leadingCoeff) ^ (b.natDegree - c.natDegree - 1)))) * c

The lower end of a degree gap, with its exact scalar. For three consecutive signed remainders, the subresultant at deg c is the displayed multiple of c. The power of -lc(c) records the size of the gap from deg b to deg c. Only the initial pair additionally requires deg q ≤ m.