OAI/Analysis/KadisonKastler/StateScalingAlgebra.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Algebraic operations on state-scaling operators

The balance identity is the bounded-operator form of a modular eigenvector. Its products, adjoints and centralizer compressions are proved directly.

  1. def OAI.KadisonKastler.StateScales line 21
  2. theorem OAI.KadisonKastler.StateScales.add line 29
  3. theorem OAI.KadisonKastler.StateScales.smul line 35
  4. theorem OAI.KadisonKastler.StateScales.mul line 40
  5. theorem OAI.KadisonKastler.StateScales.conjugate_state line 51
  6. theorem OAI.KadisonKastler.StateScales.adjoint line 57
  7. theorem OAI.KadisonKastler.StateScales.of_centralizer line 71
  8. theorem OAI.KadisonKastler.StateScales.initial_centralizes line 76
  9. theorem OAI.KadisonKastler.StateScales.final_centralizes line 83
  10. theorem OAI.KadisonKastler.StateScales.initial_state line 90
  11. theorem OAI.KadisonKastler.PointedMatrixSites.site_stateScales line 96