Symmetrization.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct line 30
Source documentation
The product of character values in the six orders of possibly different legs.
```
def sixfoldProduct (T : Tensor ℂ X Y Z) : ℝ :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_cyclic line 39
Source documentation
Cycling the legs permutes the six factors.
```
theorem sixfoldProduct_cyclic (T : Tensor ℂ X Y Z) :
    χ.sixfoldProduct (fun y z x => T x y z) = χ.sixfoldProduct T := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_swap12 line 45
Source documentation
Exchanging the first two legs permutes the six factors.
```
theorem sixfoldProduct_swap12 (T : Tensor ℂ X Y Z) :
    χ.sixfoldProduct (fun y x z => T x y z) = χ.sixfoldProduct T := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_swap23 line 51
Source documentation
The leg exchange used by the middle convolution branch preserves the product.
```
theorem sixfoldProduct_swap23 (T : Tensor ℂ X Y Z) :
    χ.sixfoldProduct (fun x z y => T x y z) = χ.sixfoldProduct T := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_reindex line 57

Source documentation

Changing coordinates separately on the legs preserves the sixfold product.

theorem sixfoldProduct_reindex (T : Tensor ℂ X Y Z)
    (ex : X' ≃ X) (ey : Y' ≃ Y) (ez : Z' ≃ Z) :
    χ.sixfoldProduct (Tensor.pullback ex ey ez T) = χ.sixfoldProduct T := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_convolution_comm line 81
Source documentation
Commuting convolution inputs preserves the sixfold character product.
```
theorem sixfoldProduct_convolution_comm (a b : ℕ) :
    χ.sixfoldProduct (convolution a b) = χ.sixfoldProduct (convolution b a) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile line 94
Source documentation
The Section 5 symmetrized value with mean singleton-leg exponent t.
```
def symmetrizedProfile (t : ℝ) (T : Tensor ℂ X Y Z) : ℝ :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_cyclic line 97
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_swap12 line 101
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_swap23 line 105
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_reindex line 109