OAI/Analysis/KadisonKastler/StateBicentralizerLocal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform reference-vector tests for the state bicentralizer

Faithfulness allows the reference-vector test to extend to every vector. The sequential condition is then equivalent to a uniform estimate for unitaries with sufficiently small state commutator.

  1. theorem OAI.KadisonKastler.stateBicentralizerMember_of_unitary_reference_tests line 22
  2. theorem OAI.KadisonKastler.stateBicentralizerMember_iff_local_reference line 43