CanonicalAmplificationGap.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The canonical amplification gap from common matrix units

Actual countable matrix units transport under a Hilbert-space isometry. Thus the common-matrix-unit gap estimate applies to the canonical Hilbert sum of the original representation, retaining its original tolerance.

instance OAI.KadisonKastler.FullMatrixCorner.spatialTransportSubspaceComplete line 26
def OAI.KadisonKastler.FullMatrixCorner.spatialTransport line 31
Source documentation
Transport of all the matrix units, including the strong sum condition.
```
def spatialTransport (e : H ≃ₗᵢ[ℂ] K) :
    FullMatrixCorner (D.map e.toLinearEquiv.toLinearMap) where
…
```
Mentions: OAI.KadisonKastler.FullMatrixCorner
theorem OAI.KadisonKastler.FullMatrixCorner.spatialTransport_entry line 55
theorem OAI.KadisonKastler.FullMatrixCorner.spatialTransport_entry_mem line 58
theorem OAI.KadisonKastler.kkDistance_canonicalAmplifiedAlgebra_le_of_common_matrix_units line 67
Source documentation
Countably many common original matrix units control the actual canonical countable amplification with the same gap.
```
theorem kkDistance_canonicalAmplifiedAlgebra_le_of_common_matrix_units
    (M N : VonNeumannAlgebra H) (F : FullMatrixCorner D)
    (hM : ∀ i j, F.entry i j ∈ M) (hN : ∀ i j, F.entry i j ∈ N) :
    kkDistance (canonicalAmplifiedAlgebra H M) (canonicalAmplifiedAlgebra H N) ≤
      kkDistance M N := by
…
```
Mentions: OAI.KadisonKastler.FullMatrixCorner, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.canonicalAmplifiedAlgebra