SixfoldProductBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_product line 26
Source documentation
Taking the product over all six leg orders preserves tensor multiplication.
```
theorem sixfoldProduct_product (T : Tensor ℂ X Y Z) (S : Tensor ℂ U V W) :
    χ.sixfoldProduct (Tensor.product T S) = χ.sixfoldProduct T * χ.sixfoldProduct S := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_nonneg line 39
Source documentation
All six factors of the symmetrized product are nonnegative.
```
theorem sixfoldProduct_nonneg (T : Tensor ℂ X Y Z) : 0 ≤ χ.sixfoldProduct T := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.one_le_sixfoldProduct line 44
Source documentation
Every nonzero tensor has symmetrized character product at least one.
```
theorem one_le_sixfoldProduct {T : Tensor ℂ X Y Z} (hT : T ≠ 0) :
    1 ≤ χ.sixfoldProduct T := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_pos line 72
Source documentation
In particular, the sixfold product of a nonzero tensor is positive.
```
theorem sixfoldProduct_pos {T : Tensor ℂ X Y Z} (hT : T ≠ 0) :
    0 < χ.sixfoldProduct T :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.rankAtMost_swap12 line 76
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_le_rank line 88
Source documentation
A rank decomposition bounds each of the six character factors.
```
theorem sixfoldProduct_le_rank {T : Tensor ℂ X Y Z} {r : ℕ}
    (h : Tensor.RankAtMost T r) : χ.sixfoldProduct T ≤ (r : ℝ) ^ 6 := by
…
```