Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.AuxiliarySeparation.Growth.PermutationProduct

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.

source
@[reducible, inline]
abbrev MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation :
Type

A permutation of the three tensor legs.

Equations
Instances For
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.card :
    Fintype.card LegPermutation = 6

    There are six orders of the three legs.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.prod_mul_right {M : Type u_1} [CommMonoid M] (f : LegPermutation → M) (σ : LegPermutation) :
    ∏ π : LegPermutation, f (π * σ) = ∏ π : LegPermutation, f π

    Right composition just reindexes a product over all six permutations.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.prod_mul_left {M : Type u_1} [CommMonoid M] (f : LegPermutation → M) (σ : LegPermutation) :
    ∏ π : LegPermutation, f (σ * π) = ∏ π : LegPermutation, f π

    Left composition also just reindexes the six factors.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.prod_trans_right {M : Type u_1} [CommMonoid M] (f : LegPermutation → M) (σ : LegPermutation) :
    ∏ π : LegPermutation, f (Equiv.trans π σ) = ∏ π : LegPermutation, f π

    The same reindexing statement in explicit equivalence-composition notation.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.sum_mul_right {A : Type u_1} [AddCommMonoid A] (f : LegPermutation → A) (σ : LegPermutation) :
    ∑ π : LegPermutation, f (π * σ) = ∑ π : LegPermutation, f π

    A permutation-independent sum may likewise be reindexed on the right.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.card_apply_fiber (i j : Fin 3) :
    Fintype.card { π : LegPermutation // π i = j } = 2

    Each original leg occurs twice in each fixed position.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.prod_apply {M : Type u_1} [CommMonoid M] (f : Fin 3 → M) (i : Fin 3) :
    ∏ π : LegPermutation, f (π i) = (∏ j : Fin 3, f j) ^ 2

    The product of values attached to one slot contains each leg twice.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.sum_apply {A : Type u_1} [AddCommMonoid A] (p : Fin 3 → A) (i : Fin 3) :
    ∑ π : LegPermutation, p (π i) = 2 • ∑ j : Fin 3, p j

    The exponent attached to one slot contains each leg exponent twice.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.prod_symm {M : Type u_1} [CommMonoid M] (f : LegPermutation → M) :
    ∏ π : LegPermutation, f (Equiv.symm π) = ∏ π : LegPermutation, f π

    Inverting the permutation preserves the symmetrized product.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.sum_symm {A : Type u_1} [AddCommMonoid A] (f : LegPermutation → A) :
    ∑ π : LegPermutation, f (Equiv.symm π) = ∑ π : LegPermutation, f π

    Inverting the permutation preserves a sum over all six orders.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.sum_symm_apply {A : Type u_1} [AddCommMonoid A] (p : Fin 3 → A) (i : Fin 3) :
    ∑ π : LegPermutation, p ((Equiv.symm π) i) = 2 • ∑ j : Fin 3, p j

    The twice-per-leg count is independent of the permutation convention.

    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.sum_exponents (p : Fin 3 → ℝ) (i : Fin 3) (t : ℝ) (h : ∑ j : Fin 3, p j = 3 * t) :
    ∑ π : LegPermutation, p (π i) = 6 * t

    The sum of the six singleton-leg exponents is six times their mean.

    source
    def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.orbitProduct {X : Type u_1} {M : Type u_2} [CommMonoid M] (transform : LegPermutation → X → X) (value : X → M) (x : X) :
    M

    The product of the valuations of all six transforms of an object.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.LegPermutation.orbitProduct_transform {X : Type u_1} {M : Type u_2} [CommMonoid M] (transform : LegPermutation → X → X) (value : X → M) (compose : ∀ (π σ : LegPermutation) (x : X), transform π (transform σ x) = transform (π * σ) x) (σ : LegPermutation) (x : X) :
      orbitProduct transform value (transform σ x) = orbitProduct transform value x

      A further leg transformation preserves the product whenever transforms compose.