Algebra and bounds for the sixfold character product #
The product over all six leg orders is multiplicative and nonnegative. A nonzero tensor has product at least one, and every rank decomposition bounds the product by the sixth power of its size.
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_product
{K : Type}
[Field K]
(χ : Character K)
{X Y Z U V W : Type}
[Fintype X]
[Fintype Y]
[Fintype Z]
[Fintype U]
[Fintype V]
[Fintype W]
(T : Foundation.Tensor K X Y Z)
(S : Foundation.Tensor K U V W)
:
Taking the product over all six leg orders preserves tensor multiplication.
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_nonneg
{K : Type}
[Field K]
(χ : Character K)
{X Y Z : Type}
[Fintype X]
[Fintype Y]
[Fintype Z]
(T : Foundation.Tensor K X Y Z)
:
All six factors of the symmetrized product are nonnegative.
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.one_le_sixfoldProduct
{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)
:
Every nonzero tensor has symmetrized character product at least one.
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_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)
:
In particular, the sixfold product of a nonzero tensor is positive.
theorem
MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_le_rank
{K : Type}
[Field K]
(χ : Character K)
{X Y Z : Type}
[Fintype X]
[Fintype Y]
[Fintype Z]
{T : Foundation.Tensor K X Y Z}
{r : ℕ}
(h : T.RankAtMost r)
:
A rank decomposition bounds each of the six character factors.