OAI/Analysis/KadisonKastler/StateUnitaryCentralizer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

State and vector unitary tests for the bicentralizer

The constructed two-sided norm estimates identify the two sequential centrality tests. The resulting characterization retains all ambient vector tests in the definition of the bicentralizer.

  1. theorem OAI.KadisonKastler.unitary_centrality_iff_state_commutator line 33
  2. theorem OAI.KadisonKastler.vectorBicentralizerMember_iff_state_unitary_tests line 52