MatrixSmallCorner.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The distinguished scalar matrix corner has the original algebra's commutator estimate on a finite standard multiplicity. The proof uses actual coordinate insertion/projection and then transports the estimate to the normalized matrix GNS space.

def OAI.KadisonSimilarity.coordinateCornerOperator line 19
Source documentation
Place one operator in a diagonal coordinate of a Hilbert array.
```
def coordinateCornerOperator {n : ℕ} (i : Fin n) (T : H →L[ℂ] H) :
    HilbertCopies H n →L[ℂ] HilbertCopies H n :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.coordinateCornerOperator_apply line 23
theorem OAI.KadisonSimilarity.norm_coordinateCornerOperator_le line 28
Source documentation
A diagonal coordinate placement is contractive.
```
theorem norm_coordinateCornerOperator_le {n : ℕ} (i : Fin n) (T : H →L[ℂ] H) :
    ‖coordinateCornerOperator i T‖ ≤ ‖T‖ := by
…
```
Mentions: OAI.KadisonSimilarity.coordinateCornerOperator
theorem OAI.KadisonSimilarity.commutator_coordinateCornerOperator line 37
Source documentation
A diagonal amplification preserves each coordinate corner.
```
theorem commutator_coordinateCornerOperator {n : ℕ} (i : Fin n)
    (Y T : H →L[ℂ] H) :
    commutator (amplify Y n) (coordinateCornerOperator i T) =
      coordinateCornerOperator i (commutator Y T) := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.coordinateCornerOperator
def OAI.KadisonSimilarity.matrixCornerProjection line 51
Source documentation
A diagonal scalar matrix unit in the actual C-star matrix algebra.
```
def matrixCornerProjection (i : Fin n) : CStarMatrix (Fin n) (Fin n) A :=
…
```
theorem OAI.KadisonSimilarity.matrixCornerProjection_isStarProjection line 55
theorem OAI.KadisonSimilarity.matrixCornerProjection_sandwich line 70
theorem OAI.KadisonSimilarity.matrixCorner_eq_single line 82
Source documentation
There is only one possibly nonzero entry in the distinguished corner.
```
theorem matrixCorner_eq_single (i : Fin n)
    (X : CStarCorner (matrixCornerProjection (A := A) i)
…
```
Mentions: OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.matrixCornerProjection
theorem OAI.KadisonSimilarity.matrixLeftArray_single line 92
theorem OAI.KadisonSimilarity.matrix_array_small_corner_bound line 104
Source documentation
The concrete distinguished corner estimate on ordinary Hilbert arrays.
```
theorem matrix_array_small_corner_bound (τ : A →ₚ[ℂ] ℂ) (i : Fin n)
    (Y : HilbertCopies τ.GNS n →L[ℂ] HilbertCopies τ.GNS n)
    {ε : ℝ} (hε : 0 ≤ ε)
    (hbound : ∀ a : A, ‖commutator Y (amplify (τ.gnsStarAlgHom a) n)‖ ≤ ε * ‖a‖)
    (X : CStarCorner (matrixCornerProjection (A := A) i)
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.matrixCornerProjection
def OAI.KadisonSimilarity.matrixGNSLiftOperator line 121
Source documentation
The amplified standard-copy operator transported to matrix GNS.
```
def matrixGNSLiftOperator (τ : A →ₚ[ℂ] ℂ)
    (Y : HilbertCopies τ.GNS n →L[ℂ] HilbertCopies τ.GNS n) :
    (normalizedMatrixTrace τ n).GNS →L[ℂ] (normalizedMatrixTrace τ n).GNS :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.normalizedMatrixTrace
theorem OAI.KadisonSimilarity.matrixGNSLiftOperator_apply line 127

theorem OAI.KadisonSimilarity.matrixGNSLiftOperator_commutator line 137

Source documentation

The transported commutator has precisely the array action.

theorem matrixGNSLiftOperator_commutator (τ : A →ₚ[ℂ] ℂ)
    (Y : HilbertCopies τ.GNS n →L[ℂ] HilbertCopies τ.GNS n)
    (X : CStarMatrix (Fin n) (Fin n) A) (ξ : (normalizedMatrixTrace τ n).GNS) :
    matrixGNSUnitary τ n
      (commutator (matrixGNSLiftOperator τ Y) ((normalizedMatrixTrace τ n).gnsStarAlgHom X) ξ) =
    commutator (amplify Y n) (matrixLeftArray τ X) (matrixGNSUnitary τ n ξ) := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.matrixGNSUnitary, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.matrixGNSLiftOperator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.matrixLeftArray

theorem OAI.KadisonSimilarity.matrix_gns_small_corner_bound line 147
Source documentation
The distinguished-corner estimate on the actual normalized matrix GNS space.
```
theorem matrix_gns_small_corner_bound (τ : A →ₚ[ℂ] ℂ) (i : Fin n)
    (Y : HilbertCopies τ.GNS n →L[ℂ] HilbertCopies τ.GNS n)
    {ε : ℝ} (hε : 0 ≤ ε)
    (hbound : ∀ a : A, ‖commutator Y (amplify (τ.gnsStarAlgHom a) n)‖ ≤ ε * ‖a‖)
    (X : CStarCorner (matrixCornerProjection (A := A) i)
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.matrixCornerProjection