The symmetrized tensor-character product

The sixfold product is defined on arbitrary finite, possibly different, leg spaces. Its symmetry follows by permuting the factors and requires no symmetry of the character itself.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : ℝ

The product of character values in the six orders of possibly different legs.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_cyclic {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : (χ.sixfoldProduct fun (y : Y) (z : Z) (x : X) => T x y z) = χ.sixfoldProduct T

Cycling the legs permutes the six factors.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_swap12 {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : (χ.sixfoldProduct fun (y : Y) (x : X) (z : Z) => T x y z) = χ.sixfoldProduct T

Exchanging the first two legs permutes the six factors.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_swap23 {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : (χ.sixfoldProduct fun (x : X) (z : Z) (y : Y) => T x y z) = χ.sixfoldProduct T

The leg exchange used by the middle convolution branch preserves the product.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_reindex {K : Type} [Field K] (χ : Character K) {X Y Z X' Y' Z' : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] (T : Foundation.Tensor K X Y Z) (ex : X' ≃ X) (ey : Y' ≃ Y) (ez : Z' ≃ Z) : χ.sixfoldProduct (Foundation.Tensor.pullback (⇑ex) (⇑ey) (⇑ez) T) = χ.sixfoldProduct T

Changing coordinates separately on the legs preserves the sixfold product.

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

Commuting convolution inputs preserves the sixfold character product.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (t : ℝ) (T : Foundation.Tensor K X Y Z) : ℝ

The Section 5 symmetrized value with mean singleton-leg exponent t.

Equations

• χ.symmetrizedProfile t T = χ.sixfoldProduct T ^ (1 / (6 * t))

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_cyclic {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (t : ℝ) (T : Foundation.Tensor K X Y Z) : (χ.symmetrizedProfile t fun (y : Y) (z : Z) (x : X) => T x y z) = χ.symmetrizedProfile t T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_swap12 {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (t : ℝ) (T : Foundation.Tensor K X Y Z) : (χ.symmetrizedProfile t fun (y : Y) (x : X) (z : Z) => T x y z) = χ.symmetrizedProfile t T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_swap23 {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (t : ℝ) (T : Foundation.Tensor K X Y Z) : (χ.symmetrizedProfile t fun (x : X) (z : Z) (y : Y) => T x y z) = χ.symmetrizedProfile t T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_reindex {K : Type} [Field K] (χ : Character K) {X Y Z X' Y' Z' : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype X'] [Fintype Y'] [Fintype Z'] (t : ℝ) (T : Foundation.Tensor K X Y Z) (ex : X' ≃ X) (ey : Y' ≃ Y) (ez : Z' ≃ Z) : χ.symmetrizedProfile t (Foundation.Tensor.pullback (⇑ex) (⇑ey) (⇑ez) T) = χ.symmetrizedProfile t T