OAI/Analysis/KadisonKastler/FixedTensorAbsorption.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.algebraEquivOfAlgebraEq line 17
2. def OAI.KadisonKastler.rightTensorEquivOfTransport line 23
3. theorem OAI.KadisonKastler.TwoRatioProductModel.tensor_absorbs_powers line 41

   Source documentation

   The fixed factor absorbs the Powers product even after tensoring with an arbitrary represented algebra. Both reassociation and changing the second tensor leg are implemented on the actual Hilbert spaces.

   theorem TwoRatioProductModel.tensor_absorbs_powers (P : TwoRatioProductModel.{u})
       (hProduct : PublishedPointedMatrixOperations.{u}) (hK : PublishedKaplanskyDensity.{u})
       (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
       (M : VonNeumannAlgebra H) :
       ∃ R : PointedMatrixProduct.{u} (fun _ : ℕ => fixedProductLambda),
         Nonempty (Algebra (spatialProductAlgebra (spatialProductAlgebra M P.stages.algebra)
           R.algebra) ≃⋆ₐ[ℂ] Algebra (spatialProductAlgebra M P.stages.algebra)) := by
   …

   Mentions: OAI.KadisonKastler.fixedProductLambda, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.spatialProductAlgebra