OAI/Analysis/KadisonKastler/ModularFixedVectors.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed vectors of the constructed modular group

The half-eigenspace of the bounded graph resolvent is fixed by every regularized group and by its strong limit. It contains the state vector and the vectors obtained from elements of the vector-state centralizer.

  1. theorem OAI.KadisonKastler.cfcHom_half_eigen line 24
  2. theorem OAI.KadisonKastler.cfc_half_eigen line 55
  3. theorem OAI.KadisonKastler.regularizedModularGroup_fixes_half_eigen line 70
  4. theorem OAI.KadisonKastler.modularStrongGroup_fixes_half_eigen line 89
  5. theorem OAI.KadisonKastler.modularStrongGroup_fixes_state line 100
  6. theorem OAI.KadisonKastler.modularStrongGroup_fixes_centralizer_vector line 106