CanonicalAmplification.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Spatial transport and the canonical infinite amplification

Transport into the initial coordinate preserves the unit balls and their Hausdorff distance. The abstract diagonal action obtained from the matrix units is exactly the coordinatewise action on the Hilbert direct sum.

theorem OAI.KadisonKastler.centralizer_image_spatial line 21
def OAI.KadisonKastler.spatialTransportAlgebra line 39
Source documentation
The concrete algebra transported by a Hilbert-space isometry.
```
def spatialTransportAlgebra (e : H ≃ₗᵢ[ℂ] K) (M : VonNeumannAlgebra H) :
    VonNeumannAlgebra K where
…
```
theorem OAI.KadisonKastler.mem_spatialTransportAlgebra line 48
theorem OAI.KadisonKastler.norm_spatialConjugate line 59
theorem OAI.KadisonKastler.unitBall_spatialTransportAlgebra line 63
theorem OAI.KadisonKastler.kkDistance_spatialTransportAlgebra line 74
Source documentation
Hilbert-space transport does not change the ordinary operator gap.
```
theorem kkDistance_spatialTransportAlgebra (e : H ≃ₗᵢ[ℂ] K)
    (M N : VonNeumannAlgebra H) :
    kkDistance (spatialTransportAlgebra e M) (spatialTransportAlgebra e N) =
      kkDistance M N := by
…
```
Mentions: OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.spatialTransportAlgebra
def OAI.KadisonKastler.spatialTransportHom line 83
theorem OAI.KadisonKastler.spatialTransportHom_bijective line 88
def OAI.KadisonKastler.spatialTransportEquiv line 99
theorem OAI.KadisonKastler.spatialTransportEquiv_apply line 103
theorem OAI.KadisonKastler.spatialTransportAlgebra_isII1 line 107
def OAI.KadisonKastler.canonicalCornerAlgebra line 116
Source documentation
The original algebra in the first coordinate of its countable sum.
```
def canonicalCornerAlgebra (M : VonNeumannAlgebra H) :
    VonNeumannAlgebra (canonicalInitialSpace H) :=
…
```
Mentions: OAI.KadisonKastler.canonicalInitialSpace
def OAI.KadisonKastler.canonicalAmplifiedAlgebra line 121
Source documentation
The countable amplification formed from the actual coordinate matrix units.
```
def canonicalAmplifiedAlgebra (M : VonNeumannAlgebra H) :
    VonNeumannAlgebra (CountableHilbertSum H) :=
…
```
Mentions: OAI.KadisonKastler.CountableHilbertSum
theorem OAI.KadisonKastler.canonicalMatrixCorner_inflate line 125
theorem OAI.KadisonKastler.l2DiagonalHom_injective line 135
theorem OAI.KadisonKastler.norm_l2Diagonal line 144
theorem OAI.KadisonKastler.l2Diagonal_mem_canonicalAmplifiedAlgebra line 148
Source documentation
Every original operator acts coordinatewise in the canonical amplification.
```
theorem l2Diagonal_mem_canonicalAmplifiedAlgebra {M : VonNeumannAlgebra H}
    {T : H →L[ℂ] H} (hT : T ∈ M) : l2Diagonal T ∈ canonicalAmplifiedAlgebra H M := by
…
```
Mentions: OAI.KadisonKastler.l2Diagonal, OAI.KadisonKastler.canonicalAmplifiedAlgebra
theorem OAI.KadisonKastler.canonicalMatrixUnit_mem_canonicalAmplifiedAlgebra line 154
theorem OAI.KadisonKastler.kkDistance_canonicalCornerAlgebra line 159