OAI/Analysis/KadisonKastler/SpatialStateHomogeneity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Vector-state comparison under a spatial algebra isomorphism

  1. theorem OAI.KadisonKastler.intertwines_of_unitaryConj line 19
  2. theorem OAI.KadisonKastler.functional_norm_eq_of_starEquiv line 29
  3. theorem OAI.KadisonKastler.spatial_vectorFunctional line 52
  4. theorem OAI.KadisonKastler.spatial_stateCommutator_norm line 57
  5. theorem OAI.KadisonKastler.FaithfulVectorStateHomogeneity.spatial_transport line 65