Dot-product exponents of tensor characters

The power laws here follow from restriction monotonicity and tensor products. They are not additional assumptions on a character. The three exponents refer to the leg on which the corresponding dot product has dimension one.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_pos {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] {T : Foundation.Tensor K X Y Z} (hT : T ≠ 0) : 0 < χ.value T

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

Precomposing a character with a cyclic permutation gives a character.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.cyclicCharacter_value {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : χ.cyclicCharacter.value T = χ.value T.cyclic

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_dotPairing_pos {K : Type} [Field K] (χ : Character K) {m : ℕ} (hm : 0 < m) : 0 < χ.value (Foundation.Tensor.dotPairing (Fin m))

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_dotPairing_le {K : Type} [Field K] (χ : Character K) (m : ℕ) : χ.value (Foundation.Tensor.dotPairing (Fin m)) ≤ ↑m

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_dotPairing_mono {K : Type} [Field K] (χ : Character K) {m n : ℕ} (hmn : m ≤ n) : χ.value (Foundation.Tensor.dotPairing (Fin m)) ≤ χ.value (Foundation.Tensor.dotPairing (Fin n))

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_dotPairing_mul {K : Type} [Field K] (χ : Character K) (m n : ℕ) : χ.value (Foundation.Tensor.dotPairing (Fin (m * n))) = χ.value (Foundation.Tensor.dotPairing (Fin m)) * χ.value (Foundation.Tensor.dotPairing (Fin n))

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

The exponent on dot products whose third leg has dimension one.

Equations

• χ.pZ = Real.log (χ.value (MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dotPairing (Fin 2))) / Real.log 2

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

The exponent on dot products whose second leg has dimension one.

Equations

• χ.pY = χ.cyclicCharacter.pZ

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

The exponent on dot products whose first leg has dimension one.

Equations

• χ.pX = χ.cyclicCharacter.cyclicCharacter.pZ

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

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

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

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

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

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_dotPairing {K : Type} [Field K] (χ : Character K) {m : ℕ} (hm : 0 < m) : χ.value (Foundation.Tensor.dotPairing (Fin m)) = ↑m ^ χ.pZ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_cyclic_dotPairing {K : Type} [Field K] (χ : Character K) {m : ℕ} (hm : 0 < m) : χ.value (Foundation.Tensor.dotPairing (Fin m)).cyclic = ↑m ^ χ.pY

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_cyclic_cyclic_dotPairing {K : Type} [Field K] (χ : Character K) {m : ℕ} (hm : 0 < m) : χ.value (Foundation.Tensor.dotPairing (Fin m)).cyclic.cyclic = ↑m ^ χ.pX

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_matrixCoefficients {K : Type} [Field K] (χ : Character K) {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : χ.value (Foundation.Tensor.matrixCoefficients (Fin a) (Fin b) (Fin c)) = ↑b ^ χ.pZ * ↑a ^ χ.pY * ↑c ^ χ.pX

Exact factorization through the three oriented dot products.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_matrixCoefficients_square {K : Type} [Field K] (χ : Character K) {m : ℕ} (hm : 0 < m) : χ.value (Foundation.Tensor.matrixCoefficients (Fin m) (Fin m) (Fin m)) = ↑m ^ (χ.pX + χ.pY + χ.pZ)

The character of square matrix multiplication has exponent pX + pY + pZ.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_matrixMultiplication {K : Type} [Field K] (χ : Character K) {m : ℕ} (hm : 0 < m) : χ.value (Foundation.Tensor.matMul K m m m) = ↑m ^ (χ.pX + χ.pY + χ.pZ)

The same power law in the matrix-tensor notation used for exact rank.