OAI/Analysis/KadisonKastler/BicentralizerStateMembership.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The state-transport limit belongs to the target bicentralizer

A diagonal choice of comparing unitaries transfers each asymptotically central unitary sequence to the source state. Faithfulness then extends the reference-vector conclusion to the whole represented Hilbert space.

  1. theorem OAI.KadisonKastler.conjugate_commutator line 23
  2. theorem OAI.KadisonKastler.unitary_commutator_vector_difference_le line 30
  3. theorem OAI.KadisonKastler.stateBicentralizerMember_of_state_conjugate_limit line 50