OAI/Analysis/KadisonKastler/SelfAdjointVectorWitness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Self-adjoint two-vector witnesses

The real and imaginary parts are controlled on the two specified vectors, rather than in operator norm. This is the reduction used before the spectral cuts in Haagerup's Lemma 2.10.

  1. theorem OAI.KadisonKastler.adjoint_vector_norm_le_defect line 20
  2. theorem OAI.KadisonKastler.realPart_vector_norm_le line 32
  3. theorem OAI.KadisonKastler.imaginaryPart_vector_norm_le line 42
  4. theorem OAI.KadisonKastler.exists_selfAdjoint_two_vector_gap line 53
  5. theorem OAI.KadisonKastler.exists_selfAdjoint_relative_two_vector line 79
  6. theorem OAI.KadisonKastler.ModularConjugationData.selfAdjoint_symmetric_vector_witness line 107