Finite differences, derivatives and resultants of univariate polynomials

Main results

• Polynomial.natDegree_comp_X_add_C_sub_self and Polynomial.leadingCoeff_comp_X_add_C_sub_self: in characteristic zero, the finite difference P(X + s) - P(X) of a polynomial of degree m + 1 with step s ≠ 0 has degree m and leading coefficient P.leadingCoeff * (m + 1) * s.
• Polynomial.derivative_ne_zero_of_natCast_natDegree_ne_zero: a polynomial whose degree is nonzero in the coefficient ring has nonzero derivative.
• Polynomial.exists_divided_difference: the divided difference (f(y) - f(z)) / (y - z) exists and is congruent to f'(z) modulo y - z.
• Matrix.natDegree_det_le, Polynomial.natDegree_resultant_le: degree bounds for determinants and Sylvester resultants of polynomials in a coefficient parameter, independent of the eliminated variable.
• Polynomial.resultant_ne_zero_of_irreducible_of_natDegree_lt: padding the second Sylvester degree preserves nonvanishing when the first polynomial is irreducible.

theorem Polynomial.natDegree_comp_X_add_C_sub_self {K : Type u_1} [Field K] [CharZero K] (P : Polynomial K) {m : ℕ} (hm : P.natDegree = m + 1) (s : K) (hs : s ≠ 0) : (P.comp (X + C s) - P).natDegree = m

In characteristic zero, the finite difference P(X + s) - P(X) with step s ≠ 0 lowers the degree by exactly one.

theorem Polynomial.leadingCoeff_comp_X_add_C_sub_self {K : Type u_1} [Field K] [CharZero K] (P : Polynomial K) {m : ℕ} (hm : P.natDegree = m + 1) (s : K) (hs : s ≠ 0) : (P.comp (X + C s) - P).leadingCoeff = P.leadingCoeff * (↑m + 1) * s

In characteristic zero, the finite difference P(X + s) - P(X) with step s ≠ 0 of a polynomial of degree m + 1 has leading coefficient P.leadingCoeff * (m + 1) * s.

theorem Polynomial.derivative_ne_zero_of_natCast_natDegree_ne_zero {R : Type u_1} [Semiring R] [NoZeroDivisors R] {f : Polynomial R} (hn : ↑f.natDegree ≠ 0) : derivative f ≠ 0

A polynomial whose degree n satisfies (n : R) ≠ 0 has nonzero derivative.

theorem Polynomial.exists_divided_difference {R : Type u_1} [CommRing R] (f : Polynomial R) (y z : R) : ∃ (q : R), eval y f - eval z f = (y - z) * q ∧ y - z ∣ q - eval z (derivative f)

Divided differences agree with the derivative modulo the argument difference.

theorem Matrix.natDegree_det_le {R : Type u_1} {ι : Type u_2} [CommRing R] [Fintype ι] [DecidableEq ι] (M : Matrix ι ι (Polynomial R)) (D : ℕ) (hM : ∀ (i j : ι), (M i j).natDegree ≤ D) : M.det.natDegree ≤ Fintype.card ι * D

The degree of a determinant of polynomials is at most the size times an entrywise degree bound.

theorem Polynomial.natDegree_resultant_le {R : Type u_1} [CommRing R] (f g : Polynomial (Polynomial R)) (m n D : ℕ) (hf : ∀ (i : ℕ), (f.coeff i).natDegree ≤ D) (hg : ∀ (i : ℕ), (g.coeff i).natDegree ≤ D) : (f.resultant g m n).natDegree ≤ (m + n) * D

The degree in the coefficient parameter of a Sylvester resultant is at most the Sylvester size times a coefficientwise degree bound.

theorem Polynomial.resultant_ne_zero_of_irreducible_of_natDegree_lt {K : Type u_1} [Field K] (f g : Polynomial K) (hf : Irreducible f) (hg : g ≠ 0) (hdeg : g.natDegree < f.natDegree) (n : ℕ) (hn : g.natDegree ≤ n) : f.resultant g f.natDegree n ≠ 0

Padding the second Sylvester degree preserves nonvanishing when the first polynomial is irreducible and the second is nonzero of smaller degree.