Polynomial convolution by evaluation and interpolation

Evaluating the two input polynomials at a + b - 1 distinct points of K, then interpolating their product, expresses the convolution tensor as a sum of a + b - 1 rank-one tensors. This is the polynomial multiplication rank upper bound used in Section 5.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.monomial_coeff_eq_sum_interpolation {K : Type} [Field K] {n m : ℕ} (hm : m < n) (v : Fin n → K) (hv : Function.Injective v) (k : ℕ) : (if m = k then 1 else 0) = ∑ r : Fin n, v r ^ m * (Lagrange.basis Finset.univ v r).coeff k

Recover each monomial coefficient from evaluations at distinct nodes.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_eq_sum_rankOne {K : Type} [Field K] {a b : ℕ} (v : Fin (a + b - 1) → K) (hv : Function.Injective v) : convolution K a b = fun (i : Fin a) (j : Fin b) (k : Fin (a + b - 1)) => ∑ r : Fin (a + b - 1), Foundation.Tensor.rankOne (fun (i : Fin a) => v r ^ ↑i) (fun (j : Fin b) => v r ^ ↑j) (fun (k : Fin (a + b - 1)) => (Lagrange.basis Finset.univ v r).coeff ↑k) i j k

Evaluation at distinct nodes and Lagrange interpolation give an explicit rank-one decomposition of polynomial convolution.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_rankAtMost {K : Type} [Field K] [IsAlgClosed K] (a b : ℕ) : (convolution K a b).RankAtMost (a + b - 1)

The convolution tensor C(a,b) has rank at most a + b - 1 over K.