OAI/Analysis/KadisonKastler/RegularCoreSpatialTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Spatial transport of the concrete regular core

Intertwining the original unitary groups transports both kinds of core generators. This result concerns the actual generated von Neumann algebras.

  1. theorem OAI.KadisonKastler.pointwiseL2Unitary_embedding_apply line 28
  2. theorem OAI.KadisonKastler.pointwiseL2Unitary_embedding line 46
  3. theorem OAI.KadisonKastler.regularCore_spatialTransport line 56
  4. theorem OAI.KadisonKastler.regularCore_equiv_of_spatial line 82