SpatialProduct.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The concrete spatial tensor product used in the fixed-factor reduction

The spatial von Neumann algebra is the bicommutant of the bounded tensor operators. Vector slices act on the completed tensor Hilbert space.

abbrev OAI.KadisonKastler.spatialLeft line 22
abbrev OAI.KadisonKastler.spatialRight line 25
def OAI.KadisonKastler.spatialProductAlgebra line 29
Source documentation
The spatial von Neumann tensor product in the given representations.
```
def spatialProductAlgebra (M : VonNeumannAlgebra H) (D : VonNeumannAlgebra K) :
    VonNeumannAlgebra (SpatialHilbert H K) :=
…
```
theorem OAI.KadisonKastler.spatialLeft_mem_product line 34
theorem OAI.KadisonKastler.spatialRight_mem_product line 45
def OAI.KadisonKastler.tensorVector line 57
Source documentation
The map inserting a fixed vector in the second tensor leg.
```
def tensorVector (ξ : K) : H →L[ℂ] SpatialHilbert H K :=
…
```
theorem OAI.KadisonKastler.tensorVector_apply line 62
theorem OAI.KadisonKastler.norm_tensorVector_apply line 67
theorem OAI.KadisonKastler.norm_tensorVector_le line 72
def OAI.KadisonKastler.tensorVectorSlice line 78
Source documentation
The vector slice is concrete compression by the tensor-vector map.
```
def tensorVectorSlice (ξ : K) :
    (SpatialHilbert H K →L[ℂ] SpatialHilbert H K) →ₗ[ℂ] (H →L[ℂ] H) where
…
```
theorem OAI.KadisonKastler.tensorVectorSlice_apply line 86
theorem OAI.KadisonKastler.tensorVectorSlice_tensor line 92
Source documentation
Slicing a simple tensor gives its actual vector-state coefficient.
```
theorem tensorVectorSlice_tensor (ξ : K) (S : H →L[ℂ] H) (T : K →L[ℂ] K) :
    tensorVectorSlice ξ (spatialTensorOp S T) = (inner ℂ ξ (T ξ)) • S := by
…
```
Mentions: OAI.KadisonKastler.tensorVectorSlice
theorem OAI.KadisonKastler.tensorVectorSlice_spatialLeft line 105
Source documentation
A unit vector makes the slice a left inverse of the first-leg inclusion.
```
theorem tensorVectorSlice_spatialLeft (ξ : K) (hξ : ‖ξ‖ = 1) (S : H →L[ℂ] H) :
    tensorVectorSlice ξ (spatialLeft S) = S := by
…
```
Mentions: OAI.KadisonKastler.tensorVectorSlice, OAI.KadisonKastler.spatialLeft
theorem OAI.KadisonKastler.norm_tensorVectorSlice_le line 112