TracialMatrixCovariance.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Actual matrix-conjugation actions on tracial tensor words

The conjugation action is constructed from the represented unitary and the tracial conjugation. Its action on completed tensor words is obtained by genuine tensor-product isometries.

def OAI.KadisonSimilarity.algebraicTensorWordIsometry line 21

Source documentation

The tensor power of an actual Hilbert-space isometry.

def algebraicTensorWordIsometry (g : F →ₗᵢ[ℂ] F) :
    (n : ℕ) → TensorWord F n →ₗᵢ[ℂ] TensorWord F n
  | 0 => LinearIsometry.id
  | n + 1 => TensorProduct.mapIsometry g (algebraicTensorWordIsometry g n)

Mentions: OAI.KadisonSimilarity.TensorWord

theorem OAI.KadisonSimilarity.algebraicTensorWordIsometry_apply line 26
def OAI.KadisonSimilarity.completedTensorWordIsometry line 35
theorem OAI.KadisonSimilarity.completedTensorWordIsometry_apply line 39
def OAI.KadisonSimilarity.endpointTensorIsometry line 49
theorem OAI.KadisonSimilarity.endpointTensorIsometry_apply line 53
def OAI.KadisonSimilarity.representedMatrixUnitary line 79
Source documentation
A matrix unitary acts isometrically through the actual left representation.
```
def representedMatrixUnitary (u : Matrix.unitaryGroup α ℂ) : E →ₗᵢ[ℂ] E :=
…
```
theorem OAI.KadisonSimilarity.representedMatrixUnitary_apply line 84
def OAI.KadisonSimilarity.tracialUnitaryConjugation line 89
Source documentation
Left multiplication followed by the conjugate right multiplication gives the actual trace-preserving matrix-conjugation isometry.
```
def tracialUnitaryConjugation (u : Matrix.unitaryGroup α ℂ) : E →ₗᵢ[ℂ] E where
…
```
theorem OAI.KadisonSimilarity.tracialUnitaryConjugation_apply_vector line 102
theorem OAI.KadisonSimilarity.tracialUnitaryConjugation_traceVector line 113
theorem OAI.KadisonSimilarity.tracialUnitaryConjugation_mem_centered line 120
def OAI.KadisonSimilarity.centeredUnitaryConjugation line 131
theorem OAI.KadisonSimilarity.tracialUnitaryConjugation_commutes line 144
theorem OAI.KadisonSimilarity.trace_matrix_conjugation line 156
theorem OAI.KadisonSimilarity.centeredUnitaryConjugation_commutes line 161

theorem OAI.KadisonSimilarity.centeredUnitaryConjugation_center line 172

Source documentation

The constructed conjugation action carries actual centered matrix vectors to the centered vectors of their matrix conjugates.

theorem centeredUnitaryConjugation_center (hτ : τ 1 = 1) (u : Matrix.unitaryGroup α ℂ)
    (a : Matrix α α ℂ) :
    centeredUnitaryConjugation τ V L ι hinner hleft htrace hdense u
      (tracialCenter V (ι a)) =
      tracialCenter V (ι ((u : Matrix α α ℂ) * a * star (u : Matrix α α ℂ))) := by
…

Mentions: OAI.KadisonSimilarity.centeredUnitaryConjugation, OAI.KadisonSimilarity.tracialCenter

theorem OAI.KadisonSimilarity.tracialUnitaryConjugation_star_matrix line 188
def OAI.KadisonSimilarity.tracialMatrixWordAction line 196
Source documentation
The genuine completed endpoint tensor action of a matrix unitary.
```
def tracialMatrixWordAction (u : Matrix.unitaryGroup α ℂ) (n : ℕ) :
    EndpointTensor E (centeredSubspace (V 1)) n →ₗᵢ[ℂ]
      EndpointTensor E (centeredSubspace (V 1)) n :=
…
```
Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.centeredSubspace

def OAI.KadisonSimilarity.tracialMatrixWordCovariance line 204

Source documentation

Actual matrix-unitary intertwining supplies the word covariance used by the finite invariant theory. The source and test word formulas are proved here.

def tracialMatrixWordCovariance (hτ : τ 1 = 1)
    (hι : ∀ a, τ (ι a) = (Fintype.card α : ℂ)⁻¹ * Matrix.trace a)
    {k l : ℕ} (Y : EndpointTensor E (centeredSubspace (V 1)) k →L[ℂ]
      EndpointTensor E (centeredSubspace (V 1)) l)
    (hY : ∀ u, Y.comp
      (tracialMatrixWordAction τ V L ι hinner hleft htrace hdense u k).toContinuousLinearMap =
      (tracialMatrixWordAction τ V L ι hinner hleft htrace hdense u l).toContinuousLinearMap.comp Y) :
    MatrixWordCovariance (tracialMatrixStage τ V L ι hinner hleft hι)
      (centeredTracialConjugation τ V hinner htrace hdense) (V 1) Y where
…

Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.tracialMatrixWordAction, OAI.KadisonSimilarity.MatrixWordCovariance, OAI.KadisonSimilarity.tracialMatrixStage, OAI.KadisonSimilarity.centeredTracialConjugation