OAI/Analysis/KadisonKastler/HaagerupProjectionWitness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Projection witnesses from the modular commutator premise

This is the bounded symmetric-vector case of Haagerup's Lemma 2.13. Both estimates concern a genuine projection in the original algebra.

  1. theorem OAI.KadisonKastler.two_vector_energy_bound line 18
  2. theorem OAI.KadisonKastler.exists_projection_of_relative_two_vector line 32
  3. theorem OAI.KadisonKastler.ModularConjugationData.symmetric_vector_projection_witness line 61
  4. theorem OAI.KadisonKastler.ModularConjugationData.symmetric_vector_nonzero_projection_witness line 85