OAI/Analysis/KadisonKastler/DominatedSymmetricWitness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Dominated symmetric vectors belong to the bounded modular core

The bounded commutant intertwiner becomes a left algebra element after conjugation. Thus the constructed projection witnesses apply exactly to every symmetric vector whose state is dominated by the reference state.

  1. theorem OAI.KadisonKastler.ModularConjugationData.exists_symmetric_algebra_vector_of_domination line 26
  2. theorem OAI.KadisonKastler.ModularConjugationData.dominated_symmetric_projection_witness line 48