OAI/Analysis/KadisonKastler/UnitaryStateDefect.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

State commutators control unitary central-vector defects

Powers–Størmer, followed by a unitary change of coordinates, gives the reverse estimate needed to compare the state and vector centralizer tests.

  1. theorem OAI.KadisonKastler.sandwich_unitary_state_norm_sub_le line 26
  2. theorem OAI.KadisonKastler.centralVectorDefect_unitary_norm_eq line 47
  3. theorem OAI.KadisonKastler.centralVectorDefect_unitary_sq_le_stateCommutator line 70