The inequalities for the polynomial profile

The six character values are combined before the common probability law is optimized. Each first-leg exponent occurs twice, so the total entropy exponent is exactly six times the mean exponent used to normalize the profile.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.permutedCharacter_meanExponent {K : Type} [Field K] (χ : Character K) (i : Fin 6) : (χ.permutedCharacter i).meanExponent = χ.meanExponent

All six permuted characters have the same mean singleton-leg exponent.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sum_permutedCharacter_pX_mean {K : Type} [Field K] (χ : Character K) : ∑ i : Fin 6, (χ.permutedCharacter i).pX = 6 * χ.meanExponent

The exponents of the six permuted characters have the normalization total.

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

All six factors associated to a positive-size polynomial tensor are positive.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.prod_permutedCharacter_swapped_convolution {K : Type} [Field K] (χ : Character K) (a b : ℕ) : (∏ i : Fin 6, (χ.permutedCharacter i).value fun (x : Fin a) (z : Fin (a + b - 1)) (y : Fin b) => convolution K a b x y z) = ∏ i : Fin 6, (χ.permutedCharacter i).value (convolution K a b)

Exchanging the two output-side positions reorders the six convolution factors.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_concave {K : Type} [Field K] (χ : Character K) [IsAlgClosed K] {a b : ℕ} (ht : 0 < χ.meanExponent) (ha : 0 < a) (hb : 2 ≤ b) : χ.convolutionProfile a (b - 1) + χ.convolutionProfile a (b + 1) ≤ 2 * χ.convolutionProfile a b

The actual polynomial profile is concave in its second positive index.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_tripling {K : Type} [Field K] (χ : Character K) [IsAlgClosed K] {a h : ℕ} (ht : 0 < χ.meanExponent) (ha : 0 < a) (hh : 0 < h) : 3 * χ.convolutionProfile a h ≤ χ.convolutionProfile a (3 * h + a - 1)

The actual three-sector degeneration triples the normalized profile.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.toScalarProfile {K : Type} [Field K] (χ : Character K) [IsAlgClosed K] (ht : 0 < χ.meanExponent) : ScalarProfile χ.meanExponent

The polynomial profile satisfies every hypothesis of the scalar growth theorem.

Equations

• χ.toScalarProfile ht = { value := χ.convolutionProfile, positive := ⋯, symmetric := ⋯, boundary := ⋯, concave := ⋯, tripling := ⋯, rank_bound := ⋯ }

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.meanExponent_le_three_quarters {K : Type} [Field K] (χ : Character K) [IsAlgClosed K] : χ.meanExponent ≤ 3 / 4

Every actual tensor character has mean singleton-leg exponent at most 3/4.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.exponent_sum_le_nine_quarters {K : Type} [Field K] (χ : Character K) [IsAlgClosed K] : χ.pX + χ.pY + χ.pZ ≤ 9 / 4

The three dot-product exponents of an actual character sum to at most 9/4.