OAI/Analysis/KadisonKastler/PositiveUnitaryTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Transporting positive matrix-central vectors by inner automorphisms

The modular quadratic unitary transports the concrete matrix algebra, its positive central vector and the associated vector state together.

  1. def OAI.KadisonKastler.modularUnitary line 25
  2. theorem OAI.KadisonKastler.modularUnitary_coe line 28
  3. theorem OAI.KadisonKastler.conjugation_modularUnitary line 32
  4. theorem OAI.KadisonKastler.modularUnitary_intertwines line 39
  5. theorem OAI.KadisonKastler.modularUnitary_right_intertwines line 55
  6. theorem OAI.KadisonKastler.modularUnitary_vectorFunctional line 64
  7. def OAI.KadisonKastler.unitaryConjugateMatrixUnits line 79
  8. theorem OAI.KadisonKastler.modularUnitary_matrix_central line 84