OAI/Analysis/KadisonKastler/PositiveConeCentralizer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

State centralizers on the constructed positive cone

A unitary centralizing a faithful positive vector state has zero central vector defect for the same conjugation. This uses positive-state uniqueness, not a new modular-conjugation identification assumption.

  1. theorem OAI.KadisonKastler.positiveCone_centralizer_unitary line 23
  2. theorem OAI.KadisonKastler.positiveCone_mem_centralVectorSpace line 73