OAI/Analysis/KadisonKastler/BicentralizerOrbitPairing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bicentralizer pairings are preserved by asymptotic orbit averages

The state commutator controls moving a unitary through the functional; the bicentralizer controls the other error on the faithful vector.

  1. theorem OAI.KadisonKastler.stateConjugate_pairing_error line 20
  2. theorem OAI.KadisonKastler.stateOrbitCore_bicentralizer_pairing line 53