CanonicalAmplificationDescent.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The coordinate slice and descent from the canonical amplification

Compression along the zeroth coordinate is an actual unital completely positive retraction of the diagonal embedding. Matrix-entry membership shows that it maps the amplified target algebra into the original one.

def OAI.KadisonKastler.operatorCompressionLinear line 33
theorem OAI.KadisonKastler.operatorCompressionLinear_apply line 39
def OAI.KadisonKastler.operatorCompressionCP line 44
Source documentation
Compression by any bounded operator is completely positive.
```
def operatorCompressionCP (S : H →L[ℂ] K) : (K →L[ℂ] K) →CP (H →L[ℂ] H) where
…
```
def OAI.KadisonKastler.canonicalSlice line 79
Source documentation
The actual completely positive coordinate-zero slice.
```
def canonicalSlice :
    (CountableHilbertSum H →L[ℂ] CountableHilbertSum H) →CP (H →L[ℂ] H) :=
…
```
Mentions: OAI.KadisonKastler.CountableHilbertSum
theorem OAI.KadisonKastler.canonicalSlice_apply line 83
theorem OAI.KadisonKastler.canonicalSlice_one line 90
theorem OAI.KadisonKastler.canonicalSlice_l2Diagonal line 94
theorem OAI.KadisonKastler.canonicalSlice_mem line 99

theorem OAI.KadisonKastler.concrete_unitary_of_canonical_amplification line 117

Source documentation

A near-identity conjugacy of the actual canonical amplifications descends through the coordinate slice to a conjugacy on the original space.

theorem concrete_unitary_of_canonical_amplification {M N : VonNeumannAlgebra H}
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (z : unitary (CountableHilbertSum H →L[ℂ] CountableHilbertSum H))
    (hz : Conjugates z (canonicalAmplifiedAlgebra H M) (canonicalAmplifiedAlgebra H N))
    {g : ℝ} (hgap : kkDistance M N < g)
    (hsmall : 2 * ‖(z : CountableHilbertSum H →L[ℂ] CountableHilbertSum H) - 1‖ < 1 / 1000)
    (hge : g + 2 * ‖(z : CountableHilbertSum H →L[ℂ] CountableHilbertSum H) - 1‖ < 1) :
    ∃ u : unitary (H →L[ℂ] H), Conjugates u M N ∧
      ‖(u : H →L[ℂ] H) - 1‖ ≤
        256 * ‖(z : CountableHilbertSum H →L[ℂ] CountableHilbertSum H) - 1‖ := by
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.CountableHilbertSum, OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.canonicalAmplifiedAlgebra, OAI.KadisonKastler.kkDistance