OAI/Analysis/KadisonKastler/SpatialProductCyclic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.ProductMatrixStages.cyclic line 17
2. theorem OAI.KadisonKastler.denseRange_spatialProduct_vector line 25

   Source documentation

   Dense orbits in each tensor leg give a dense orbit for the product vector. The proof takes place in the completed Hilbert tensor product.

   theorem denseRange_spatialProduct_vector
       (M : VonNeumannAlgebra H) (D : VonNeumannAlgebra K) (Ω : H) (ξ : K)
       (hM : DenseRange (algebraVectorMap M Ω))
       (hD : DenseRange (algebraVectorMap D ξ)) :
       DenseRange (algebraVectorMap (spatialProductAlgebra M D) (tensorVector ξ Ω)) := by
   …

   Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.tensorVector