TensorDiagonalWeights.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Diagonal unitary phases separate the multiplicity weights of a finite tensor power. This is the weight calculation in the Schur--Weyl argument.

def OAI.KadisonSimilarity.tensorLabelCount line 17
Source documentation
The multiplicity of a label in an elementary tensor.
```
def tensorLabelCount (f : ι → α) (a : α) : ℕ := Fintype.card {i // f i = a}
…
```
theorem OAI.KadisonSimilarity.tensorLabelCount_le line 20
theorem OAI.KadisonSimilarity.prod_labels_eq line 24
theorem OAI.KadisonSimilarity.tupleTensorMatrix_diagonal line 30
def OAI.KadisonSimilarity.tensorDiagonalUnitary line 39
Source documentation
A scalar diagonal whose entries lie on the unit circle.
```
def tensorDiagonalUnitary (d : α → unitary ℂ) : Matrix.unitaryGroup α ℂ :=
…
```
def OAI.KadisonSimilarity.tensorRoot line 53
theorem OAI.KadisonSimilarity.phase_product line 68

theorem OAI.KadisonSimilarity.tensor_commutant_entry_zero_of_weight_ne line 76

Source documentation

Distinct label multiplicities cannot occur in the support of an operator commuting with all tensor powers of unitaries.

theorem tensor_commutant_entry_zero_of_weight_ne
    (C : Matrix (ι → α) (ι → α) ℂ)
    (hC : ∀ u : Matrix.unitaryGroup α ℂ,
      C * tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) =
        tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) * C)
    (f g : ι → α) (a : α) (hne : tensorLabelCount f a ≠ tensorLabelCount g a) :
    C f g = 0 := by
…

Mentions: OAI.KadisonSimilarity.tupleTensorMatrix, OAI.KadisonSimilarity.tensorLabelCount

theorem OAI.KadisonSimilarity.tensor_commutant_commutes_diagonal line 102

Source documentation

Every complex diagonal commutes with the tensor commutant; the unit-circle condition on the testing diagonals has disappeared.

theorem tensor_commutant_commutes_diagonal
    (C : Matrix (ι → α) (ι → α) ℂ)
    (hC : ∀ u : Matrix.unitaryGroup α ℂ,
      C * tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) =
        tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) * C)
    (d : α → ℂ) :
    C * tupleTensorMatrix (fun _ : ι => Matrix.diagonal d) =
      tupleTensorMatrix (fun _ : ι => Matrix.diagonal d) * C := by
…

Mentions: OAI.KadisonSimilarity.tupleTensorMatrix