The polynomial multiplication tensor

The coefficient tensor convolution a b represents multiplication of binary forms of degrees a - 1 and b - 1, or equivalently ordinary coefficient convolution. The output leg has a + b - 1 coordinates. The definitions also make sense when an input dimension is zero, while the nonzero and full-output-support statements use the positive dimensions assumed in Section 5 of the paper.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution (K : Type) [Field K] (a b : ℕ) : Foundation.Tensor K (Fin a) (Fin b) (Fin (a + b - 1))

The tensor C(a,b) of Section 5, in monomial coefficient coordinates.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution K a b i j k = if ↑i + ↑j = ↑k then 1 else 0

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_apply {K : Type} [Field K] (a b : ℕ) (i : Fin a) (j : Fin b) (k : Fin (a + b - 1)) : convolution K a b i j k = if ↑i + ↑j = ↑k then 1 else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_ne_zero_iff {K : Type} [Field K] {a b : ℕ} (i : Fin a) (j : Fin b) (k : Fin (a + b - 1)) : convolution K a b i j k ≠ 0 ↔ ↑i + ↑j = ↑k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_eq_one_iff {K : Type} [Field K] {a b : ℕ} (i : Fin a) (j : Fin b) (k : Fin (a + b - 1)) : convolution K a b i j k = 1 ↔ ↑i + ↑j = ↑k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_eq_zero_iff {K : Type} [Field K] {a b : ℕ} (i : Fin a) (j : Fin b) (k : Fin (a + b - 1)) : convolution K a b i j k = 0 ↔ ↑i + ↑j ≠ ↑k

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolutionOutput {a b : ℕ} (i : Fin a) (j : Fin b) : Fin (a + b - 1)

Every pair of input monomials has a valid output coordinate.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolutionOutput i j = ⟨↑i + ↑j, ⋯⟩

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_at_output {K : Type} [Field K] {a b : ℕ} (i : Fin a) (j : Fin b) : convolution K a b i j (convolutionOutput i j) = 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_output_supported {K : Type} [Field K] {a b : ℕ} (ha : 0 < a) (hb : 0 < b) (k : Fin (a + b - 1)) : ∃ (i : Fin a) (j : Fin b), convolution K a b i j k = 1

Every output monomial of the expected degree occurs in the product.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_nonzero {K : Type} [Field K] {a b : ℕ} (ha : 0 < a) (hb : 0 < b) : convolution K a b ≠ 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_nonzero_iff {K : Type} [Field K] (a b : ℕ) : convolution K a b ≠ 0 ↔ 0 < a ∧ 0 < b

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_comm {K : Type} [Field K] (a b : ℕ) (i : Fin a) (j : Fin b) (k : Fin (a + b - 1)) : convolution K a b i j k = convolution K b a j i (Fin.cast ⋯ k)

Commuting the two inputs only casts the equal output dimensions.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_one_left {K : Type} [Field K] (b : ℕ) (i : Fin 1) (j : Fin b) (k : Fin (1 + b - 1)) : convolution K 1 b i j k = if ↑j = ↑k then 1 else 0

The boundary tensor C(1,b) has the coefficient matrix of a dot product.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_one_right {K : Type} [Field K] (a : ℕ) (i : Fin a) (j : Fin 1) (k : Fin (a + 1 - 1)) : convolution K a 1 i j k = if ↑i = ↑k then 1 else 0

The other boundary tensor has the same coordinate identity.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolutionOneOutputEquiv (b : ℕ) : Fin b ≃ Fin (1 + b - 1)

Relabel the output of C(1,b) by its actual dimension b.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolutionOneOutputEquiv b = finCongr ⋯

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolutionOneInputEquiv : Unit ≃ Fin 1

Relabel the single input coordinate of C(1,b) by Unit.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_one_left_dotPairing {K : Type} [Field K] (b : ℕ) : Foundation.Tensor.pullback (⇑convolutionOneInputEquiv) (⇑(Equiv.refl (Fin b))) (⇑(convolutionOneOutputEquiv b)) (convolution K 1 b) = (Foundation.Tensor.dotPairing (Fin b)).cyclic.cyclic

C(1,b) is the dot-product tensor with the singleton on the first leg.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolutionRightOneOutputEquiv (a : ℕ) : Fin a ≃ Fin (a + 1 - 1)

Relabel the output of C(a,1) by its actual dimension a.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolutionRightOneOutputEquiv a = finCongr ⋯

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_one_right_dotPairing {K : Type} [Field K] (a : ℕ) : Foundation.Tensor.pullback (⇑(Equiv.refl (Fin a))) (⇑convolutionOneInputEquiv) (⇑(convolutionRightOneOutputEquiv a)) (convolution K a 1) = (Foundation.Tensor.dotPairing (Fin a)).cyclic

C(a,1) is the dot-product tensor with the singleton on the second leg.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.contract_convolution {K : Type} [Field K] {a b : ℕ} (x : Fin a → K) (y : Fin b → K) (k : Fin (a + b - 1)) : (convolution K a b).contract x y k = ∑ i : Fin a, ∑ j : Fin b, if ↑i + ↑j = ↑k then x i * y j else 0

Contracting the coefficient tensor computes ordinary finite convolution.