CanonicalMatrixCorner.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The canonical countable matrix corner

The coordinate injections and evaluations on the Hilbert direct sum give actual matrix units. Their initial corner is canonically isometric to the original Hilbert space, and their diagonal projections sum strongly to the identity.

def OAI.KadisonKastler.canonicalSingle line 19
def OAI.KadisonKastler.canonicalCoordinate line 22
theorem OAI.KadisonKastler.canonicalSingle_apply line 25
theorem OAI.KadisonKastler.canonicalCoordinate_apply line 28
def OAI.KadisonKastler.canonicalMatrixUnit line 31
theorem OAI.KadisonKastler.canonicalMatrixUnit_apply line 34
theorem OAI.KadisonKastler.canonicalMatrixUnit_mul line 37
def OAI.KadisonKastler.canonicalInitialSpace line 47
Source documentation
The closed subspace supported at coordinate zero.
```
def canonicalInitialSpace : Submodule ℂ (CountableHilbertSum H) :=
…
```
Mentions: OAI.KadisonKastler.CountableHilbertSum
theorem OAI.KadisonKastler.mem_canonicalInitialSpace line 50
def OAI.KadisonKastler.canonicalInitialEquiv line 54
Source documentation
The initial coordinate has exactly the original Hilbert norm.
```
def canonicalInitialEquiv : H ≃ₗᵢ[ℂ] canonicalInitialSpace H where
…
```
Mentions: OAI.KadisonKastler.canonicalInitialSpace
theorem OAI.KadisonKastler.canonicalInitialEquiv_apply line 74
theorem OAI.KadisonKastler.canonicalInitialEquiv_symm_apply line 77
instance OAI.KadisonKastler.canonicalInitialSpaceComplete line 82
theorem OAI.KadisonKastler.canonicalSingle_adjoint line 86
theorem OAI.KadisonKastler.canonicalMatrixUnit_star line 93
theorem OAI.KadisonKastler.canonicalMatrixUnit_zero_zero line 100
def OAI.KadisonKastler.canonicalMatrixCorner line 114
Source documentation
The standard countable matrix units on the Hilbert direct sum.
```
def canonicalMatrixCorner : FullMatrixCorner (canonicalInitialSpace H) where
…
```
Mentions: OAI.KadisonKastler.FullMatrixCorner, OAI.KadisonKastler.canonicalInitialSpace
theorem OAI.KadisonKastler.canonicalMatrixCorner_entry line 121
theorem OAI.KadisonKastler.canonicalMatrixCorner_column line 124
theorem OAI.KadisonKastler.canonicalMatrixCorner_matrixEntry line 131