OAI/Analysis/KadisonKastler/HaagerupBoundedVectorWitness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Two-vector witnesses on the algebraic symmetric core

This is the bounded-vector part of Haagerup's Lemma 2.9. The constants are deliberately loose; they remain uniform over the algebra and vector.

  1. theorem OAI.KadisonKastler.ModularConjugationData.commutator_norm_le_vector_defects line 22
  2. theorem OAI.KadisonKastler.ModularConjugationData.bounded_symmetric_vector_witness line 37