Principal subresultant coefficients

This file defines the fixed-bound principal subresultant coefficient of two polynomials. For j ≤ min m n, its matrix is obtained from the Sylvester matrix by deleting the first and last j rows and the last j columns from each polynomial block. Thus the coefficient at index zero is the resultant, while the terminal coefficient is a power of the coefficient at the smaller bound.

Keeping the bounds explicit is essential for specialization: mapping coefficients commutes with the construction even when the degrees of the mapped polynomials drop. These determinants are the scalar data used by subresultant gcd criteria and projection operators.

Main results

• TauCeti.coefficientRow_dotProduct: a row of shifted polynomial coefficients reads any coefficient of A * q + B * p from the coefficient vector of (A, B).
• Polynomial.subresultantMatrix_mulVec: the matrix acts on a pair of coefficient vectors as (A, B) ↦ A * q + B * p, its row i reading the coefficient of degree i + j.
• Polynomial.psc_zero: the zeroth principal subresultant coefficient is the resultant.
• Polynomial.psc_map_map: fixed-bound principal subresultant coefficients commute with coefficient maps.
• Polynomial.psc_comm: swapping the polynomials multiplies by (-1) ^ ((m - j) * (n - j)).
• Polynomial.psc_C_mul_left, Polynomial.psc_C_mul_right: scaling one polynomial by a constant scales the coefficient by a power of that constant.
• Polynomial.psc_left_bound, Polynomial.psc_right_bound: at a formal degree bound, the determinant is a power of the coefficient at that bound.
• Polynomial.psc_min: the terminal determinant is a power of the coefficient at the smaller degree bound.

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.subresultantMatrix {R : Type u_1} [Semiring R] (p q : Polynomial R) (m n j : ℕ) : Matrix (Fin (m - j + (n - j))) (Fin (m - j + (n - j))) R

The square coefficient matrix whose determinant is the principal subresultant coefficient at index j and formal degree bounds m and n.

Row i reads the coefficient of degree i + j. The first m - j columns read q, X*q, ..., X^(m-j-1)*q and the last n - j columns read p, X*p, ..., X^(n-j-1)*p, with q and p truncated to their formal bounds n and m; when q.natDegree ≤ n and p.natDegree ≤ m the entries are exactly those coefficients (Polynomial.subresultantMatrix_apply_eq_coeff). For j ≤ min m n, the case subresultant applications use, the rows read the degrees j, ..., m+n-j-1.

Equations

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

@[simp]

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

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

@[simp]

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

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

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

When the formal bounds dominate the degrees, subresultant entries are simply coefficients of the shifted input polynomials.

@[simp]

theorem Polynomial.subresultantMatrix_zero {R : Type u_1} [Semiring R] (p q : Polynomial R) (m n : ℕ) : p.subresultantMatrix q m n 0 = p.sylvester q m n

At index zero, the principal subresultant matrix is Mathlib's Sylvester matrix.

@[simp]

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

Mapping coefficients maps every entry of the fixed-bound principal subresultant matrix.

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

Swapping the polynomials and their bounds swaps the two column blocks of the principal subresultant matrix.

theorem TauCeti.coefficientRow_dotProduct {R : Type u_1} [CommSemiring R] [DecidableEq R] {p q : Polynomial R} {m n : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (a b d : ℕ) (v : Fin (a + b) → R) : (fun (i : Fin (a + b)) => Fin.addCases (fun (l : Fin a) => if ↑l ≤ d ∧ d ≤ ↑l + n then q.coeff (d - ↑l) else 0) (fun (l : Fin b) => if ↑l ≤ d ∧ d ≤ ↑l + m then p.coeff (d - ↑l) else 0) i) ⬝ᵥ v = (((Polynomial.ofFn a) fun (l : Fin a) => v (Fin.castAdd b l)) * q + ((Polynomial.ofFn b) fun (l : Fin b) => v (Fin.natAdd a l)) * p).coeff d

A row of coefficients of shifted q and p reads the coefficient of degree d of A * q + B * p, where the two blocks of v are the coefficients of A and B. The row lengths are arbitrary, and the formal bounds dominate the actual input degrees.

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

The principal subresultant matrix acts on a vector as the linear map (A, B) ↦ A * q + B * p, where A and B are the polynomials whose coefficients are the first m - j and the last n - j entries of the vector: entry i of the result is the coefficient of degree i + j. The formal bounds must dominate the actual degrees.

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

The principal subresultant coefficient at index j and formal degree bounds m and n.

The bounds are part of the data: they are not recomputed after coefficient specialization.

Equations

• p.psc q m n j = (p.subresultantMatrix q m n j).det

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

The principal subresultant coefficient is the determinant of the principal subresultant matrix.

@[simp]

theorem Polynomial.psc_zero {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n : ℕ) : p.psc q m n 0 = p.resultant q m n

The zeroth principal subresultant coefficient is the fixed-bound resultant.

@[simp]

theorem Polynomial.psc_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).psc (map f q) m n j = f (p.psc q m n j)

Principal subresultant coefficients commute with coefficient maps at fixed bounds. No degree-preservation hypothesis is needed.

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

Swapping the polynomials and their bounds changes the principal subresultant coefficient by the sign (-1) ^ ((m - j) * (n - j)).

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

Scaling the left polynomial by a constant r scales its n - j columns, hence the principal subresultant coefficient, by r ^ (n - j).

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

Scaling the right polynomial by a constant r scales its m - j columns, hence the principal subresultant coefficient, by r ^ (m - j).

@[simp]

theorem Polynomial.psc_left_bound {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n : ℕ) : p.psc q m n m = p.coeff m ^ (n - m)

At the left formal degree bound, the principal coefficient is the corresponding power of the left polynomial's coefficient. This is the terminal coefficient when m ≤ n; when n < m, both sides reduce to 1 because the index is beyond the subresultant range.

@[simp]

theorem Polynomial.psc_right_bound {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n : ℕ) : p.psc q m n n = q.coeff n ^ (m - n)

At the right formal degree bound, the principal coefficient is the corresponding power of the right polynomial's coefficient. This is the terminal coefficient when n ≤ m; when m < n, both sides reduce to 1 because the index is beyond the subresultant range.

@[simp]

theorem Polynomial.psc_min {R : Type u_1} [CommRing R] (p q : Polynomial R) (m n : ℕ) : p.psc q m n (min m n) = if m ≤ n then p.coeff m ^ (n - m) else q.coeff n ^ (m - n)

The principal coefficient at the terminal subresultant index is a power of the coefficient at the smaller formal degree bound.