CornerCuntzFamily.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Common isometries from countable matrix units

Regrouping the countably many matrix summands gives the finite Cuntz families used to identify matrix unit balls with ordinary unit balls. The isometries belong to every von Neumann algebra containing the matrix units, by their explicit strong-sum formula.

theorem OAI.KadisonKastler.FullMatrixCorner.ext_on_columns line 29
theorem OAI.KadisonKastler.FullMatrixCorner.eq_of_inner_columns line 42
def OAI.KadisonKastler.FullMatrixCorner.regroupedColumns line 56
theorem OAI.KadisonKastler.FullMatrixCorner.regroupedColumns_orthogonal line 58
def OAI.KadisonKastler.FullMatrixCorner.regroupingIsometry line 66
Source documentation
The isometry sending matrix summand k to summand e (i,k).
```
def regroupingIsometry (i : n) : H →ₗᵢ[ℂ] H :=
…
```
theorem OAI.KadisonKastler.FullMatrixCorner.regroupingIsometry_column line 69
def OAI.KadisonKastler.FullMatrixCorner.regroupingOperator line 76
theorem OAI.KadisonKastler.FullMatrixCorner.regroupingOperator_column line 79
theorem OAI.KadisonKastler.FullMatrixCorner.adjoint_regrouping_column line 85
theorem OAI.KadisonKastler.FullMatrixCorner.regrouping_orthogonal line 104
theorem OAI.KadisonKastler.FullMatrixCorner.regrouping_total line 114
def OAI.KadisonKastler.FullMatrixCorner.cuntzFamily line 125
Source documentation
This construction is independent of the algebra that contains the matrix units, so the same family can be used on both sides of a gap.
```
def cuntzFamily : CuntzFamily n H where
…
```
Mentions: OAI.KadisonKastler.CuntzFamily
theorem OAI.KadisonKastler.FullMatrixCorner.regroupingOperator_mem line 131
theorem OAI.KadisonKastler.FullMatrixCorner.cuntzFamily_mem line 151
def OAI.KadisonKastler.FullMatrixCorner.finiteCuntz line 157
Source documentation
Every positive matrix size is obtained from the same countable matrix units by the quotient-and-remainder bijection.
```
def finiteCuntz (n : ℕ) [NeZero n] : CuntzFamily (Fin n) H :=
…
```
Mentions: OAI.KadisonKastler.CuntzFamily
theorem OAI.KadisonKastler.FullMatrixCorner.finiteCuntz_mem line 160
theorem OAI.KadisonKastler.FullMatrixCorner.matrix_hausdorffDist_eq line 166
Source documentation
There is no growth in the perturbation tolerance at any positive matrix size when both algebras contain these countable matrix units.
```
theorem matrix_hausdorffDist_eq (n : ℕ) [NeZero n] (M N : VonNeumannAlgebra H)
    (hM : ∀ i j, F.entry i j ∈ M) (hN : ∀ i j, F.entry i j ∈ N) :
    Metric.hausdorffDist (CuntzFamily.matrixUnitBall (n := Fin n) M)
…
```
Mentions: OAI.KadisonKastler.CuntzFamily.matrixUnitBall