SpatialTensorDescent.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Removing the auxiliary spatial tensor factor

A concrete unit vector slice removes the auxiliary factor. Thus an upstairs unitary yields an original-space unitary with the explicit UCP descent bound.

def OAI.KadisonKastler.tensorVectorSliceCP line 36

Source documentation

The concrete vector slice is completely positive.

def tensorVectorSliceCP (ξ : K) :
    (SpatialHilbert H K →L[ℂ] SpatialHilbert H K) →CP (H →L[ℂ] H) :=
…

theorem OAI.KadisonKastler.tensorVectorSliceCP_apply line 42
theorem OAI.KadisonKastler.spatialLeft_injective_of_unit_vector line 47
Source documentation
A unit vector makes the first-leg representation faithful.
```
theorem spatialLeft_injective_of_unit_vector (ξ : K) (hξ : ‖ξ‖ = 1) :
    Function.Injective (spatialLeft (H := H) (K := K)) := by
…
```
Mentions: OAI.KadisonKastler.spatialLeft

theorem OAI.KadisonKastler.concrete_unitary_of_spatial_product_conjugacy line 54

Source documentation

The tensor-factor removal estimate, on the original Hilbert space.

theorem concrete_unitary_of_spatial_product_conjugacy
    {M N : VonNeumannAlgebra H} (D : VonNeumannAlgebra K)
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (ξ : K) (hξ : ‖ξ‖ = 1)
    (z : unitary (SpatialHilbert H K →L[ℂ] SpatialHilbert H K))
    (hz : Conjugates z (spatialProductAlgebra M D) (spatialProductAlgebra N D))
    {g : ℝ} (hgap : kkDistance M N < g)
    (hsmall : 2 * ‖(z : SpatialHilbert H K →L[ℂ] SpatialHilbert H K) - 1‖ < 1 / 1000)
    (hge : g + 2 * ‖(z : SpatialHilbert H K →L[ℂ] SpatialHilbert H K) - 1‖ < 1) :
    ∃ u : unitary (H →L[ℂ] H), Conjugates u M N ∧
      ‖(u : H →L[ℂ] H) - 1‖ ≤
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.kkDistance