OAI/Analysis/KadisonKastler/StateCentralizerVonNeumann.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact vector-state centralizer as a von Neumann algebra

Strong approximation preserves its defining matrix-coefficient identities. The reference vector restricts to a faithful trace. For the fixed product construction, finite-site swaps make this centralizer a factor.

  1. def OAI.KadisonKastler.stateCentralizerAlgebra line 26
  2. theorem OAI.KadisonKastler.stateCentralizerAlgebra_bicommutant line 57
  3. def OAI.KadisonKastler.stateCentralizerVonNeumann line 80
  4. theorem OAI.KadisonKastler.stateCentralizerVonNeumann_le line 84
  5. def OAI.KadisonKastler.stateCentralizerTrace line 87
  6. theorem OAI.KadisonKastler.ProductMatrixStages.stateCentralizer_scalarCenter line 99