CuntzMatrices.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Matrix amplification using common isometries

A finite Cuntz family gives an actual star equivalence between the ambient operator algebra and its matrix amplification. If its isometries belong to two concrete algebras, the same equivalence identifies both matrix unit balls with their original unit balls.

structure OAI.KadisonKastler.CuntzFamily line 25

Source documentation

A finite family of isometries with orthogonal ranges summing to one.

structure CuntzFamily (n : Type*) [Fintype n] [DecidableEq n] (H : Type*)
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] where
…

def OAI.KadisonKastler.CuntzFamily.matrix line 38
def OAI.KadisonKastler.CuntzFamily.assemble line 41
theorem OAI.KadisonKastler.CuntzFamily.assemble_matrix line 44
theorem OAI.KadisonKastler.CuntzFamily.matrix_assemble line 53
theorem OAI.KadisonKastler.CuntzFamily.matrix_mul line 64
def OAI.KadisonKastler.CuntzFamily.matrixHom line 77
theorem OAI.KadisonKastler.CuntzFamily.matrixHom_injective line 90
def OAI.KadisonKastler.CuntzFamily.matrixEquiv line 96
theorem OAI.KadisonKastler.CuntzFamily.norm_matrix line 100
theorem OAI.KadisonKastler.CuntzFamily.norm_assemble line 103
theorem OAI.KadisonKastler.CuntzFamily.matrix_mem line 106
theorem OAI.KadisonKastler.CuntzFamily.assemble_mem line 110
def OAI.KadisonKastler.CuntzFamily.matrixUnitBall line 116
Source documentation
The concrete matrix unit ball uses the C*-matrix norm.
```
def matrixUnitBall (M : VonNeumannAlgebra H) : Set (CStarMatrix n n (H →L[ℂ] H)) :=
…
```
theorem OAI.KadisonKastler.CuntzFamily.matrixUnitBall_image line 119
theorem OAI.KadisonKastler.CuntzFamily.matrix_hausdorffDist_eq line 132
Source documentation
The matrix-level Hausdorff distance is exactly the ordinary distance when the same Cuntz family belongs to both algebras.
```
theorem matrix_hausdorffDist_eq (M N : VonNeumannAlgebra H)
    (hM : ∀ i, S.entry i ∈ M) (hN : ∀ i, S.entry i ∈ N) :
    Metric.hausdorffDist (matrixUnitBall (n := n) M) (matrixUnitBall (n := n) N) =
…
```
Mentions: OAI.KadisonKastler.CuntzFamily.matrixUnitBall

theorem OAI.KadisonKastler.CuntzFamily.exists_matrix_unitBall_approx line 142

Source documentation

Common isometries transport an ordinary unit-ball approximant to a matrix unit-ball approximant with precisely the same error.

theorem exists_matrix_unitBall_approx (M N : VonNeumannAlgebra H)
    (hM : ∀ i, S.entry i ∈ M) (hN : ∀ i, S.entry i ∈ N)
    {r : ℝ} (hr : kkDistance M N < r)
    (X : CStarMatrix n n (H →L[ℂ] H)) (hX : ∀ i j, X i j ∈ M) (hXnorm : ‖X‖ ≤ 1) :
    ∃ Y : CStarMatrix n n (H →L[ℂ] H), (∀ i j, Y i j ∈ N) ∧
      ‖Y‖ ≤ 1 ∧ ‖X - Y‖ < r := by
…

Mentions: OAI.KadisonKastler.kkDistance