Confluent Hermite interpolation from Taylor jets

A polynomial of degree less than Q * J is determined by its first J Taylor coefficients at each of Q nodes, provided the nodes differ by units. Over a commutative ring R, the order-J Taylor jet of p at nodes t : Fin Q → R is the family of coefficients (Polynomial.taylor (t i) p).coeff j = [z ^ j] p (t i + z), for i < Q and j < J (Polynomial.taylorJet). This file proves

• uniqueness: a polynomial of degree less than Q * J whose jet vanishes is zero, over any commutative ring whose nodes have unit differences (Polynomial.eq_zero_of_taylorJet_eq_zero);
• reconstruction: for integer nodes, the integer confluent Vandermonde matrix Polynomial.hermiteMatrix maps the coefficient vector to the jet, it is nonsingular when the nodes are distinct, and Cramer's rule expresses each coefficient through two determinants (Polynomial.det_hermiteMatrix_mul_coeff). Over a ℚ-algebra this recovers every coefficient, and in particular the value at 0, as a rational combination of the jet (Polynomial.eval_zero_eq_of_taylorJet).

The coefficient of X ^ u is indexed by c : Fin Q × Fin J with u = finProdFinEquiv c, so the Hermite matrix is square over Fin Q × Fin J. Its entry in row (i, j) and column c is (u choose j) * t i ^ (u - j), the coefficient of z ^ j in (t i + z) ^ u; it vanishes for u < j because the binomial does.

This is the interpolation step of the subexponential counting algorithm of [OAI26c] (§3.4 and Appendix B.3): the count is the value at 0 of a polynomial H of degree less than Q * J, and only Taylor coefficients of H at the nodes 1, …, Q are computed. Ordinary Lagrange interpolation (Lagrange.interpolate) is the case J = 1.

Main definitions

• Polynomial.taylorJet: the order-J Taylor jet at Q nodes, as a linear map.
• Polynomial.hermiteMatrix: the integer confluent Vandermonde matrix of integer nodes.

Main results

• Polynomial.eq_zero_of_taylorJet_eq_zero, Polynomial.eq_of_taylorJet_eq: uniqueness.
• Polynomial.hermiteMatrix_mulVec: the Hermite matrix maps coefficients to the jet.
• Polynomial.det_hermiteMatrix_ne_zero: it is nonsingular at distinct integer nodes.
• Polynomial.det_hermiteMatrix_mul_coeff: Cramer's rule for the coefficients, over any commutative ring.
• Polynomial.coeff_eq_of_taylorJet, Polynomial.eval_zero_eq_of_taylorJet: reconstruction over a ℚ-algebra.

References

• OpenAI, The Exponential Time Hypothesis is False

Taylor jets and uniqueness

noncomputable def Polynomial.taylorJet {R : Type u_1} [CommRing R] {Q : ℕ} (t : Fin Q → R) (J : ℕ) : Polynomial R →ₗ[R] Fin Q × Fin J → R

The order-J Taylor jet of a polynomial at the nodes t: the coefficient of z ^ j in p (t i + z), for i < Q and j < J.

@[simp]

theorem Polynomial.taylorJet_apply {R : Type u_1} [CommRing R] {Q : ℕ} (t : Fin Q → R) (J : ℕ) (p : Polynomial R) (r : Fin Q × Fin J) : (taylorJet t J) p r = ((taylor (t r.1)) p).coeff ↑r.2

theorem Polynomial.eq_zero_of_taylorJet_eq_zero {R : Type u_1} [CommRing R] {Q J : ℕ} {t : Fin Q → R} (ht : Pairwise fun (i j : Fin Q) => IsUnit (t i - t j)) {p : Polynomial R} (hp : p.degree < ↑(Q * J)) (h : (taylorJet t J) p = 0) : p = 0

Uniqueness of confluent Hermite interpolation. A polynomial of degree less than Q * J whose order-J Taylor jet vanishes at Q nodes with unit differences is zero.

theorem Polynomial.eq_of_taylorJet_eq {R : Type u_1} [CommRing R] {Q J : ℕ} {t : Fin Q → R} (ht : Pairwise fun (i j : Fin Q) => IsUnit (t i - t j)) {p q : Polynomial R} (hp : p.degree < ↑(Q * J)) (hq : q.degree < ↑(Q * J)) (h : (taylorJet t J) p = (taylorJet t J) q) : p = q

Two polynomials of degree less than Q * J with the same order-J Taylor jet at Q nodes with unit differences are equal.

The Hermite matrix and reconstruction

def Polynomial.hermiteMatrix {Q : ℕ} (t : Fin Q → ℤ) (J : ℕ) : Matrix (Fin Q × Fin J) (Fin Q × Fin J) ℤ

The integer confluent Vandermonde (Hermite) matrix of the nodes t: the entry in row (i, j) and column c is (u choose j) * t i ^ (u - j) with u = finProdFinEquiv c, the coefficient of z ^ j in (t i + z) ^ u.

theorem Polynomial.hermiteMatrix_apply {Q J : ℕ} (t : Fin Q → ℤ) (r c : Fin Q × Fin J) : hermiteMatrix t J r c = ↑((↑(finProdFinEquiv c)).choose ↑r.2) * t r.1 ^ (↑(finProdFinEquiv c) - ↑r.2)

theorem Polynomial.hermiteMatrix_mulVec {R : Type u_1} [CommRing R] {Q J : ℕ} (t : Fin Q → ℤ) {p : Polynomial R} (hp : p.degree < ↑(Q * J)) : (((hermiteMatrix t J).map Int.cast).mulVec fun (c : Fin Q × Fin J) => p.coeff ↑(finProdFinEquiv c)) = (taylorJet (fun (i : Fin Q) => ↑(t i)) J) p

The Hermite matrix maps coefficients to the jet. For p of degree less than Q * J, the Hermite matrix applied to the vector of coefficients of X ^ (finProdFinEquiv c) is the order-J Taylor jet of p at the nodes, over any commutative ring.

theorem Polynomial.det_hermiteMatrix_ne_zero {Q J : ℕ} {t : Fin Q → ℤ} (ht : Function.Injective t) : (hermiteMatrix t J).det ≠ 0

The Hermite matrix is nonsingular at distinct integer nodes.

theorem Polynomial.det_hermiteMatrix_mul_coeff {R : Type u_1} [CommRing R] {Q J : ℕ} (t : Fin Q → ℤ) {p : Polynomial R} (hp : p.degree < ↑(Q * J)) (c : Fin Q × Fin J) : ↑(hermiteMatrix t J).det * p.coeff ↑(finProdFinEquiv c) = (((hermiteMatrix t J).map Int.cast).updateCol c ((taylorJet (fun (i : Fin Q) => ↑(t i)) J) p)).det

Cramer's rule for confluent Hermite interpolation, over any commutative ring: for p of degree less than Q * J, the determinant of the Hermite matrix times the coefficient of X ^ (finProdFinEquiv c) is the determinant of the Hermite matrix with column c replaced by the order-J Taylor jet of p.

theorem Polynomial.coeff_eq_of_taylorJet {Q J : ℕ} (A : Type u_2) [CommRing A] [Algebra ℚ A] {t : Fin Q → ℤ} (ht : Function.Injective t) {p : Polynomial A} (hp : p.degree < ↑(Q * J)) (c : Fin Q × Fin J) : p.coeff ↑(finProdFinEquiv c) = (↑(hermiteMatrix t J).det)⁻¹ • (((hermiteMatrix t J).map Int.cast).updateCol c ((taylorJet (fun (i : Fin Q) => ↑(t i)) J) p)).det

Reconstruction over a ℚ-algebra. At distinct integer nodes, each coefficient of a polynomial of degree less than Q * J is a rational multiple of a determinant formed from the Hermite matrix and the order-J Taylor jet.

theorem Polynomial.eval_zero_eq_of_taylorJet {Q J : ℕ} (A : Type u_2) [CommRing A] [Algebra ℚ A] {t : Fin Q → ℤ} (ht : Function.Injective t) (hQ : 0 < Q) (hJ : 0 < J) {p : Polynomial A} (hp : p.degree < ↑(Q * J)) : eval 0 p = (↑(hermiteMatrix t J).det)⁻¹ • (((hermiteMatrix t J).map Int.cast).updateCol (⟨0, hQ⟩, ⟨0, hJ⟩) ((taylorJet (fun (i : Fin Q) => ↑(t i)) J) p)).det

The value at 0 from the jet (B.1). At distinct integer nodes, the value at 0 of a polynomial of degree less than Q * J, over a ℚ-algebra, is the determinant of the Hermite matrix with its column for X ^ 0 replaced by the order-J Taylor jet, divided by the determinant of the Hermite matrix.