Character identities for polynomial convolution

The boundary convolution tensors are dot products. In the sixfold character product, each possible singleton leg appears exactly twice. Consequently the normalization by the average dot-product exponent gives the boundary values of the polynomial profile from Section 5.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_dotPairing {K : Type} [Field K] (χ : Character K) (n : ℕ) : χ.sixfoldProduct (Foundation.Tensor.dotPairing (Fin n)) = (χ.value (Foundation.Tensor.dotPairing (Fin n)) * χ.value (Foundation.Tensor.dotPairing (Fin n)).cyclic * χ.value (Foundation.Tensor.dotPairing (Fin n)).cyclic.cyclic) ^ 2

A symmetric dot product occurs twice in each of its three leg positions.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_convolution_one_left {K : Type} [Field K] (χ : Character K) (b : ℕ) : χ.sixfoldProduct (convolution K 1 b) = χ.sixfoldProduct (Foundation.Tensor.dotPairing (Fin b))

The boundary C(1,b) has the sixfold product of a dot product.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_convolution_one_right {K : Type} [Field K] (χ : Character K) (a : ℕ) : χ.sixfoldProduct (convolution K a 1) = χ.sixfoldProduct (Foundation.Tensor.dotPairing (Fin a))

The boundary C(a,1) has the same dot-product product.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.meanExponent {K : Type} [Field K] (χ : Character K) : ℝ

The mean of the character's three singleton-leg exponents.

Equations

• χ.meanExponent = (χ.pX + χ.pY + χ.pZ) / 3

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.meanExponent_nonneg {K : Type} [Field K] (χ : Character K) : 0 ≤ χ.meanExponent

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.meanExponent_le_one {K : Type} [Field K] (χ : Character K) : χ.meanExponent ≤ 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_dotPairing_eq_rpow {K : Type} [Field K] (χ : Character K) {n : ℕ} (hn : 0 < n) : χ.sixfoldProduct (Foundation.Tensor.dotPairing (Fin n)) = ↑n ^ (6 * χ.meanExponent)

The three exponents occur twice in the sixfold boundary product.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_convolution_one_left_eq_rpow {K : Type} [Field K] (χ : Character K) {b : ℕ} (hb : 0 < b) : χ.sixfoldProduct (convolution K 1 b) = ↑b ^ (6 * χ.meanExponent)

The positive-size boundary product has its exact normalized power.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile {K : Type} [Field K] (χ : Character K) (a b : ℕ) : ℝ

The polynomial profile P(a,b) normalized by the actual mean exponent.

Equations

• χ.convolutionProfile a b = χ.symmetrizedProfile χ.meanExponent (MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution K a b)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_comm {K : Type} [Field K] (χ : Character K) (a b : ℕ) : χ.convolutionProfile a b = χ.convolutionProfile b a

Swapping the two polynomial inputs preserves the normalized profile.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_nonneg {K : Type} [Field K] (χ : Character K) (a b : ℕ) : 0 ≤ χ.convolutionProfile a b

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_pos {K : Type} [Field K] (χ : Character K) {a b : ℕ} (ha : 0 < a) (hb : 0 < b) : 0 < χ.convolutionProfile a b

Nonzero polynomial multiplication gives a positive normalized profile.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_le {K : Type} [Field K] (χ : Character K) [IsAlgClosed K] {a b : ℕ} (ht : 0 < χ.meanExponent) : χ.convolutionProfile a b ≤ ↑(a + b - 1) ^ (1 / χ.meanExponent)

The evaluation/interpolation algorithm bounds the normalized profile.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_one_left {K : Type} [Field K] (χ : Character K) {b : ℕ} (ht : 0 < χ.meanExponent) (hb : 0 < b) : χ.convolutionProfile 1 b = ↑b

The normalization gives the exact initial value P(1,b) = b.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_one_right {K : Type} [Field K] (χ : Character K) {a : ℕ} (ht : 0 < χ.meanExponent) (ha : 0 < a) : χ.convolutionProfile a 1 = ↑a

Input symmetry gives the other exact initial value P(a,1) = a.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_convolution_le {K : Type} [Field K] (χ : Character K) [IsAlgClosed K] (a b : ℕ) : χ.value (convolution K a b) ≤ ↑(a + b - 1)

Interpolation bounds an individual character on polynomial convolution.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_convolution_pos {K : Type} [Field K] (χ : Character K) {a b : ℕ} (ha : 0 < a) (hb : 0 < b) : 0 < χ.value (convolution K a b)

Positive input sizes give a positive individual character value.