OAI/Analysis/KadisonKastler/StateCentralSequenceAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The C-star algebra of state-central bounded sequences

State commutator estimates provide addition, multiplication, adjoints and norm closure directly, independently of the vector centrality criterion.

  1. def OAI.KadisonKastler.StateAsymptoticallyCentral line 21
  2. theorem OAI.KadisonKastler.StateAsymptoticallyCentral.add line 24
  3. theorem OAI.KadisonKastler.StateAsymptoticallyCentral.smul line 32
  4. theorem OAI.KadisonKastler.StateAsymptoticallyCentral.star line 38
  5. theorem OAI.KadisonKastler.StateAsymptoticallyCentral.mul line 43
  6. theorem OAI.KadisonKastler.stateAsymptoticallyCentral_isClosed line 53
  7. def OAI.KadisonKastler.stateCentralSequenceAlgebra line 83
  8. instance OAI.KadisonKastler.stateCentralSequenceAlgebra_complete line 101
  9. instance OAI.KadisonKastler.stateCentralSequenceAlgebra_cstar line 105