PermutationProduct.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Products over the six permutations of three tensor legs

The symmetrized quantity in Section 5 uses every permutation of the three tensor legs. Composing by a fixed permutation preserves this product. For the exponent calculation, each original leg occurs twice in any fixed slot. These are finite identities; they do not assume that an individual tensor character is invariant under exchanging its legs.

abbrev OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation line 26
Source documentation
A permutation of the three tensor legs.
```
abbrev LegPermutation := Equiv.Perm (Fin 3)
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.card line 31
Source documentation
There are six orders of the three legs.
```
theorem card : Fintype.card LegPermutation = 6 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.prod_mul_right line 35
Source documentation
Right composition just reindexes a product over all six permutations.
```
theorem prod_mul_right {M : Type*} [CommMonoid M]
    (f : LegPermutation → M) (σ : LegPermutation) :
    (∏ π, f (π * σ)) = ∏ π, f π := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.prod_mul_left line 41
Source documentation
Left composition also just reindexes the six factors.
```
theorem prod_mul_left {M : Type*} [CommMonoid M]
    (f : LegPermutation → M) (σ : LegPermutation) :
    (∏ π, f (σ * π)) = ∏ π, f π := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.prod_trans_right line 47
Source documentation
The same reindexing statement in explicit equivalence-composition notation.
```
theorem prod_trans_right {M : Type*} [CommMonoid M]
    (f : LegPermutation → M) (σ : LegPermutation) :
    (∏ π : LegPermutation, f (π.trans σ)) = ∏ π, f π := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.sum_mul_right line 53
Source documentation
A permutation-independent sum may likewise be reindexed on the right.
```
theorem sum_mul_right {A : Type*} [AddCommMonoid A]
    (f : LegPermutation → A) (σ : LegPermutation) :
    (∑ π, f (π * σ)) = ∑ π, f π := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.card_apply_fiber line 59
Source documentation
Each original leg occurs twice in each fixed position.
```
theorem card_apply_fiber (i j : Fin 3) :
    Fintype.card {π : LegPermutation // π i = j} = 2 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.prod_apply line 65
Source documentation
The product of values attached to one slot contains each leg twice.
```
theorem prod_apply {M : Type*} [CommMonoid M] (f : Fin 3 → M) (i : Fin 3) :
    (∏ π : LegPermutation, f (π i)) = (∏ j, f j) ^ 2 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.sum_apply line 71
Source documentation
The exponent attached to one slot contains each leg exponent twice.
```
theorem sum_apply {A : Type*} [AddCommMonoid A] (p : Fin 3 → A) (i : Fin 3) :
    (∑ π : LegPermutation, p (π i)) = 2 • ∑ j, p j := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.prod_symm line 77
Source documentation
Inverting the permutation preserves the symmetrized product.
```
theorem prod_symm {M : Type*} [CommMonoid M] (f : LegPermutation → M) :
    (∏ π : LegPermutation, f π.symm) = ∏ π, f π := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.sum_symm line 82
Source documentation
Inverting the permutation preserves a sum over all six orders.
```
theorem sum_symm {A : Type*} [AddCommMonoid A] (f : LegPermutation → A) :
    (∑ π : LegPermutation, f π.symm) = ∑ π, f π := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.sum_symm_apply line 87
Source documentation
The twice-per-leg count is independent of the permutation convention.
```
theorem sum_symm_apply {A : Type*} [AddCommMonoid A]
    (p : Fin 3 → A) (i : Fin 3) :
    (∑ π : LegPermutation, p (π.symm i)) = 2 • ∑ j, p j := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.sum_exponents line 93
Source documentation
The sum of the six singleton-leg exponents is six times their mean.
```
theorem sum_exponents (p : Fin 3 → ℝ) (i : Fin 3) (t : ℝ)
    (h : (∑ j, p j) = 3 * t) :
    (∑ π : LegPermutation, p (π i)) = 6 * t := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
def OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.orbitProduct line 101
Source documentation
The product of the valuations of all six transforms of an object.
```
def orbitProduct {X M : Type*} [CommMonoid M]
    (transform : LegPermutation → X → X) (value : X → M) (x : X) : M :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation
theorem OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.orbitProduct_transform line 106
Source documentation
A further leg transformation preserves the product whenever transforms compose.
```
theorem orbitProduct_transform {X M : Type*} [CommMonoid M]
    (transform : LegPermutation → X → X) (value : X → M)
    (compose : ∀ π σ x, transform π (transform σ x) = transform (π * σ) x)
    (σ : LegPermutation) (x : X) :
    orbitProduct transform value (transform σ x) = orbitProduct transform value x := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation, OAI.MatrixMultiplication.AuxiliarySeparation.LegPermutation.orbitProduct