Subresultant polynomials

This file defines the fixed-bound subresultant polynomial of two polynomials. At a strict index j < min m n, its coefficient of degree k ≤ j is the Sylvester minor obtained by replacing the first row of the principal subresultant matrix at index j by the row of coefficients of degree k; in particular, its coefficient of degree j is the principal subresultant coefficient. Outside the strict range the minors remain scalar data (for instance the terminal empty determinant recorded by psc), and the subresultant polynomial is zero.

The construction retains explicit degree bounds, so it commutes with coefficient maps even when specialization lowers the degrees. Its degree bound and top coefficient identify the scalar minor that controls the subresultant gcd criterion.

Main results

• Polynomial.subresultantCoeffMatrix_eq_updateRow: the coefficient matrix replaces the first row of the principal matrix.
• Polynomial.subresultantCoeffMatrix_mulVec: the coefficient matrix reads the coefficients of A * q + B * p, with degree k in the first row.
• Polynomial.coeff_subresultant: at a strict index j < min m n, the coefficients are the prescribed minors through degree j, and vanish above j; outside that range they all vanish.
• Polynomial.degree_subresultant_le: the subresultant polynomial has degree at most j.
• Polynomial.subresultant_map_map: fixed-bound subresultant polynomials commute with coefficient maps.
• Polynomial.subresultant_comm: swapping the inputs gives the Sylvester block-swap sign.

References

• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 4.
• Q. Vermande, Cylindrical Algebraic Decomposition in Coq/Rocq, §3.

def Polynomial.subresultantCoeffMatrix {R : Type u_1} [Semiring R] (p q : Polynomial R) (m n j k : ℕ) : Matrix (Fin (m - j + (n - j))) (Fin (m - j + (n - j))) R

The coefficient matrix whose determinant is the coefficient of degree k in the subresultant polynomial at a strict index j < min m n and formal degree bounds m and n. The matrix is defined for all indices; outside the strict range its determinant is only scalar data.

The first row of subresultantMatrix p q m n j, which reads coefficients of degree j, is replaced by the row reading coefficients of degree k. Applications use k ≤ j.

Equations

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

@[simp]

theorem Polynomial.subresultantCoeffMatrix_castAdd {R : Type u_1} [Semiring R] (p q : Polynomial R) (m n j k : ℕ) (i : Fin (m - j + (n - j))) (l : Fin (m - j)) : p.subresultantCoeffMatrix q m n j k i (Fin.castAdd (n - j) l) = have d := if ↑i = 0 then k else ↑i + j; if ↑l ≤ d ∧ d ≤ ↑l + n then q.coeff (d - ↑l) else 0

An entry in the first, q-column block of a subresultant coefficient matrix.

@[simp]

theorem Polynomial.subresultantCoeffMatrix_natAdd {R : Type u_1} [Semiring R] (p q : Polynomial R) (m n j k : ℕ) (i : Fin (m - j + (n - j))) (l : Fin (n - j)) : p.subresultantCoeffMatrix q m n j k i (Fin.natAdd (m - j) l) = have d := if ↑i = 0 then k else ↑i + j; if ↑l ≤ d ∧ d ≤ ↑l + m then p.coeff (d - ↑l) else 0

An entry in the second, p-column block of a subresultant coefficient matrix.

theorem Polynomial.subresultantCoeffMatrix_apply_eq_coeff {R : Type u_1} [Semiring R] {p q : Polynomial R} {m n : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (j k : ℕ) (i l : Fin (m - j + (n - j))) : p.subresultantCoeffMatrix q m n j k i l = Fin.addCases (fun (l : Fin (m - j)) => (X ^ ↑l * q).coeff (if ↑i = 0 then k else ↑i + j)) (fun (l : Fin (n - j)) => (X ^ ↑l * p).coeff (if ↑i = 0 then k else ↑i + j)) l

When the formal bounds dominate the input degrees, coefficient-matrix entries are coefficients of shifted input polynomials, including the replaced first row.

theorem Polynomial.subresultantCoeffMatrix_eq_updateRow {R : Type u_1} [Semiring R] (p q : Polynomial R) (m n j k : ℕ) (i₀ : Fin (m - j + (n - j))) (hi₀ : ↑i₀ = 0) : p.subresultantCoeffMatrix q m n j k = (p.subresultantMatrix q m n j).updateRow i₀ (p.subresultantCoeffMatrix q m n j k i₀)

A subresultant coefficient matrix replaces the row of degree j of the principal matrix by the row of degree k.

theorem Polynomial.subresultantCoeffMatrix_mulVec {R : Type u_1} [CommSemiring R] [DecidableEq R] {p q : Polynomial R} {m n : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (j k : ℕ) (v : Fin (m - j + (n - j)) → R) (i : Fin (m - j + (n - j))) : (p.subresultantCoeffMatrix q m n j k).mulVec v i = (((ofFn (m - j)) fun (l : Fin (m - j)) => v (Fin.castAdd (n - j) l)) * q + ((ofFn (n - j)) fun (l : Fin (n - j)) => v (Fin.natAdd (m - j) l)) * p).coeff (if ↑i = 0 then k else ↑i + j)

A subresultant coefficient matrix reads coefficients of A * q + B * p from the coefficient vector of (A, B). Its first row reads degree k; the other rows read degrees i.val + j. The formal bounds dominate the actual input degrees.

@[simp]

theorem Polynomial.subresultantCoeffMatrix_self {R : Type u_1} [Semiring R] (p q : Polynomial R) (m n j : ℕ) : p.subresultantCoeffMatrix q m n j j = p.subresultantMatrix q m n j

At k = j, the coefficient matrix is the principal subresultant matrix.

@[simp]

theorem Polynomial.subresultantCoeffMatrix_map_map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (p q : Polynomial R) (m n j k : ℕ) : (map f p).subresultantCoeffMatrix (map f q) m n j k = f.mapMatrix (p.subresultantCoeffMatrix q m n j k)

Mapping coefficients maps every entry of a fixed-bound subresultant coefficient matrix.

theorem Polynomial.subresultantCoeffMatrix_comm {R : Type u_1} [Semiring R] (p q : Polynomial R) (m n j k : ℕ) : p.subresultantCoeffMatrix q m n j k = (Matrix.reindex (finCongr ⋯) finAddFlip) (q.subresultantCoeffMatrix p n m j k)

Swapping the polynomials and bounds swaps the column blocks of every subresultant coefficient matrix.

def Polynomial.subresultantCoeff {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j k : ℕ) : R

The scalar minor used as the coefficient of degree k ≤ j in the subresultant polynomial at a strict index j < min m n. It is defined for all indices; outside the strict range it is scalar data only (the subresultant polynomial is then zero), e.g. the empty determinant 1 at m = n = j = 0.

Equations

• p.subresultantCoeff q m n j k = (p.subresultantCoeffMatrix q m n j k).det

theorem Polynomial.subresultantCoeff_def {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j k : ℕ) : p.subresultantCoeff q m n j k = (p.subresultantCoeffMatrix q m n j k).det

A subresultant coefficient is the determinant of its coefficient matrix.

@[simp]

theorem Polynomial.subresultantCoeff_right_bound {R : Type u_1} [CommRing R] (p q : Polynomial R) {m n k : ℕ} (hnm : n < m) (hk : k ≤ n) : p.subresultantCoeff q m n n k = q.coeff k * q.coeff n ^ (m - n - 1)

At the smaller right terminal index, a coefficient minor reads a coefficient of the right input times a power of its coefficient at the bound. The empty determinant is excluded.

@[simp]

theorem Polynomial.subresultantCoeff_self {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j : ℕ) : p.subresultantCoeff q m n j j = p.psc q m n j

The coefficient minor at k = j is the principal subresultant coefficient.

@[simp]

theorem Polynomial.subresultantCoeff_map_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (p q : Polynomial R) (m n j k : ℕ) : (map f p).subresultantCoeff (map f q) m n j k = f (p.subresultantCoeff q m n j k)

Subresultant coefficient minors commute with coefficient maps at fixed bounds.

theorem Polynomial.subresultantCoeff_comm {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j k : ℕ) : p.subresultantCoeff q m n j k = (-1) ^ ((m - j) * (n - j)) * q.subresultantCoeff p n m j k

Swapping the inputs changes every coefficient minor by the Sylvester block-swap sign.

@[simp]

theorem Polynomial.subresultantCoeff_left_bound {R : Type u_1} [CommRing R] (p q : Polynomial R) {m n k : ℕ} (hmn : m < n) (hk : k ≤ m) : p.subresultantCoeff q m n m k = p.coeff k * p.coeff m ^ (n - m - 1)

At the smaller left terminal index, a coefficient minor reads a coefficient of the left input times a power of its coefficient at the bound. The empty determinant is excluded.

theorem Polynomial.subresultantCoeff_C_mul_left {R : Type u_1} [CommRing R] (p q : Polynomial R) (r : R) (m n j k : ℕ) : (C r * p).subresultantCoeff q m n j k = r ^ (n - j) * p.subresultantCoeff q m n j k

Scaling the left polynomial by r scales every coefficient minor by r ^ (n - j).

theorem Polynomial.subresultantCoeff_C_mul_right {R : Type u_1} [CommRing R] (p q : Polynomial R) (r : R) (m n j k : ℕ) : p.subresultantCoeff (C r * q) m n j k = r ^ (m - j) * p.subresultantCoeff q m n j k

Scaling the right polynomial by r scales every coefficient minor by r ^ (m - j).

noncomputable def Polynomial.subresultant {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j : ℕ) : Polynomial R

The fixed-bound subresultant polynomial at index j.

Its coefficient of degree k ≤ j is subresultantCoeff p q m n j k; all coefficients above j vanish. This definition is the subresultant polynomial only at strict indices j < min m n and returns zero outside that range; terminal data, including the empty determinant, is represented by psc instead.

Equations

• p.subresultant q m n j = if j < min m n then (Polynomial.ofFn (j + 1)) fun (k : Fin (j + 1)) => p.subresultantCoeff q m n j ↑k else 0

@[simp]

theorem Polynomial.coeff_subresultant {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j k : ℕ) : (p.subresultant q m n j).coeff k = if j < min m n ∧ k ≤ j then p.subresultantCoeff q m n j k else 0

The coefficient formula for a fixed-bound subresultant polynomial.

@[simp]

theorem Polynomial.subresultant_eq_zero_of_min_le {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j : ℕ) (hj : min m n ≤ j) : p.subresultant q m n j = 0

subresultant returns zero at and beyond the terminal index min m n.

@[simp]

theorem Polynomial.subresultant_zero {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n : ℕ) (h : 0 < min m n) : p.subresultant q m n 0 = C (p.resultant q m n)

When both formal bounds are positive, the subresultant polynomial at index zero is the constant resultant.

theorem Polynomial.degree_subresultant_le {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j : ℕ) : (p.subresultant q m n j).degree ≤ ↑j

The subresultant polynomial at index j has degree at most j.

theorem Polynomial.degree_subresultant_eq_iff {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j : ℕ) (hj : j < min m n) : (p.subresultant q m n j).degree = ↑j ↔ p.psc q m n j ≠ 0

At a strict index j < min m n, the subresultant polynomial has degree exactly j precisely when its principal coefficient does not vanish.

@[simp]

theorem Polynomial.subresultant_map_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (p q : Polynomial R) (m n j : ℕ) : (map f p).subresultant (map f q) m n j = map f (p.subresultant q m n j)

Fixed-bound subresultant polynomials commute with coefficient maps. No degree-preservation hypothesis is required.

theorem Polynomial.subresultant_C_mul_left {R : Type u_1} [CommRing R] (p q : Polynomial R) (r : R) (m n j : ℕ) : (C r * p).subresultant q m n j = C (r ^ (n - j)) * p.subresultant q m n j

Scaling the left input by r scales its subresultant polynomial at index j by r ^ (n - j).

theorem Polynomial.subresultant_C_mul_right {R : Type u_1} [CommRing R] (p q : Polynomial R) (r : R) (m n j : ℕ) : p.subresultant (C r * q) m n j = C (r ^ (m - j)) * p.subresultant q m n j

Scaling the right input by r scales its subresultant polynomial at index j by r ^ (m - j).

theorem Polynomial.subresultant_comm {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n j : ℕ) : p.subresultant q m n j = C ((-1) ^ ((m - j) * (n - j))) * q.subresultant p n m j

Swapping the inputs and their bounds changes the subresultant polynomial by the Sylvester block-swap sign.