TracialSymmetryExtraction.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The centered symmetry dilation is tested on actual finite Hilbert arrays. Its original entry is recovered by coordinate insertion and projection, both contractive. Thus no matrix-size factor enters the commutator estimate.

def OAI.KadisonSimilarity.matrixEntryCompression line 22
Source documentation
An off-diagonal block of an operator on finite Hilbert arrays.
```
def matrixEntryCompression {n m : ℕ} (i : Fin m) (j : Fin n)
    (T : HilbertCopies H n →L[ℂ] HilbertCopies K m) : H →L[ℂ] K :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.matrixEntryCompression_apply line 26
theorem OAI.KadisonSimilarity.norm_matrixEntryCompression_le line 31
Source documentation
Coordinate compression is contractive, independently of the array sizes.
```
theorem norm_matrixEntryCompression_le {n m : ℕ} (i : Fin m) (j : Fin n)
    (T : HilbertCopies H n →L[ℂ] HilbertCopies K m) :
    ‖matrixEntryCompression i j T‖ ≤ ‖T‖ := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.matrixEntryCompression
theorem OAI.KadisonSimilarity.matrixEntryCompression_matrixOperator line 43
theorem OAI.KadisonSimilarity.matrixEntryCompression_commutator line 49
theorem OAI.KadisonSimilarity.norm_entry_commutator_le line 57
Source documentation
Every matrix-entry commutator is a genuine corner of the amplified one.
```
theorem norm_entry_commutator_le {n : ℕ}
    (Y : H →L[ℂ] H) (X : Matrix (Fin n) (Fin n) (H →L[ℂ] H)) (i j : Fin n) :
    ‖commutator Y (X i j)‖ ≤ ‖commutator (amplify Y n) (matrixOperator X)‖ := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.matrixOperator
def OAI.KadisonSimilarity.representedMatrix line 67
Source documentation
A C-star matrix acts entrywise on actual finite Hilbert sums.
```
def representedMatrix (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) {n : ℕ}
    (X : CStarMatrix (Fin n) (Fin n) A) :
    HilbertCopies H n →L[ℂ] HilbertCopies H n :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies

def OAI.KadisonSimilarity.entryMatrixHom line 73

Source documentation

Entrywise application of the original representation to ordinary matrices.

def entryMatrixHom (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (n : ℕ) :
    Matrix (Fin n) (Fin n) A →⋆ₐ[ℂ] Matrix (Fin n) (Fin n) (H →L[ℂ] H) where
…

def OAI.KadisonSimilarity.representedMatrixHom line 83

Source documentation

The concrete matrix action is a unital star representation.

def representedMatrixHom (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (n : ℕ) :
    CStarMatrix (Fin n) (Fin n) A →⋆ₐ[ℂ]
      (HilbertCopies H n →L[ℂ] HilbertCopies H n) :=
…

Mentions: OAI.KadisonSimilarity.HilbertCopies

theorem OAI.KadisonSimilarity.representedMatrixHom_apply line 89
def OAI.KadisonSimilarity.representedDoubleMatrix line 94
Source documentation
The four-by-four dilation acts on two successive two-coordinate sums.
```
def representedDoubleMatrix (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (S : Mat (Mat A)) :
    HilbertCopies (HilbertCopies H 2) 2 →L[ℂ] HilbertCopies (HilbertCopies H 2) 2 :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.representedDoubleMatrix_apply line 99

theorem OAI.KadisonSimilarity.double_matrix_commutator_corner line 105

Source documentation

Two successive coordinate corners recover each original algebra entry.

theorem double_matrix_commutator_corner (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (Y : H →L[ℂ] H) (S : Mat (Mat A)) (i j k l : Fin 2) :
    matrixEntryCompression k l (matrixEntryCompression i j
      (commutator (amplify (amplify Y 2) 2) (representedDoubleMatrix σ S))) =
      commutator Y (σ (S i j k l)) := by
…

Mentions: OAI.KadisonSimilarity.matrixEntryCompression, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedDoubleMatrix

theorem OAI.KadisonSimilarity.norm_double_entry_commutator_le line 121

Source documentation

The double compression has norm at most one.

theorem norm_double_entry_commutator_le (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (Y : H →L[ℂ] H) (S : Mat (Mat A)) (i j k l : Fin 2) :
    ‖commutator Y (σ (S i j k l))‖ ≤
      ‖commutator (amplify (amplify Y 2) 2) (representedDoubleMatrix σ S)‖ := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedDoubleMatrix

theorem OAI.KadisonSimilarity.centered_symmetry_commutator_corner line 133
Source documentation
The original commutator is exactly the designated double corner of the centered symmetry's commutator.
```
theorem centered_symmetry_commutator_corner (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (Y : H →L[ℂ] H) (a : A) (ha : ‖a‖ ≤ 1) :
    matrixEntryCompression 0 1 (matrixEntryCompression 0 1
      (commutator (amplify (amplify Y 2) 2)
        (representedDoubleMatrix σ (contractionSymmetryUnitary a ha)))) =
      commutator Y (σ a) := by
…
```
Mentions: OAI.KadisonSimilarity.matrixEntryCompression, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedDoubleMatrix, OAI.KadisonSimilarity.contractionSymmetryUnitary
theorem OAI.KadisonSimilarity.norm_commutator_le_centered_symmetry line 143
Source documentation
Testing the actual four-by-four centered symmetry controls the original contraction, with constant one.
```
theorem norm_commutator_le_centered_symmetry (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (Y : H →L[ℂ] H) (a : A) (ha : ‖a‖ ≤ 1) :
    ‖commutator Y (σ a)‖ ≤
      ‖commutator (amplify (amplify Y 2) 2)
        (representedDoubleMatrix σ (contractionSymmetryUnitary a ha))‖ := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedDoubleMatrix, OAI.KadisonSimilarity.contractionSymmetryUnitary
theorem OAI.KadisonSimilarity.norm_amplified_commutator_le_centered_symmetry line 153
Source documentation
In particular, a matrix commutator in the original amplification is recovered from the centered symmetry over that matrix algebra.
```
theorem norm_amplified_commutator_le_centered_symmetry
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (Y : H →L[ℂ] H) {n : ℕ} [NeZero n]
    (X : CStarMatrix (Fin n) (Fin n) A) (hX : ‖X‖ ≤ 1) :
    ‖commutator (amplify Y n) (representedMatrix σ X)‖ ≤
      ‖commutator (amplify (amplify (amplify Y n) 2) 2)
        (representedDoubleMatrix (representedMatrixHom σ n)
          (contractionSymmetryUnitary X hX))‖ :=
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.representedDoubleMatrix, OAI.KadisonSimilarity.representedMatrixHom, OAI.KadisonSimilarity.contractionSymmetryUnitary