OAI/Analysis/KadisonKastler/BicentralizerScalarStateTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Scalar bicentralizers transfer between approximately conjugate states

One scalar bicentralizer suffices under the explicitly stated faithful state homogeneity hypothesis. This does not prove that hypothesis.

  1. theorem OAI.KadisonKastler.vector_norm_sq_le_conjugate_state_distance line 22
  2. theorem OAI.KadisonKastler.scalar_bicentralizer_of_comparing_unitaries line 41
  3. theorem OAI.KadisonKastler.FaithfulVectorStateHomogeneity.scalar_bicentralizers_of_one line 80