OAI/Analysis/KadisonKastler/AngledProjectionWitness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Projection witnesses away from the reference line

The orthogonal-vector witness extends to a real unit-circle combination. The squared sine is kept as a multiplier, so no trigonometric conventions or division by a small angle enter the subsequent corner argument. This is the local estimate in Haagerup, Acta Math.158(1987), Lemma2.14.

  1. theorem OAI.KadisonKastler.norm_real_combination_sq_le line 23
  2. theorem OAI.KadisonKastler.norm_sub_sq_le_two line 34
  3. theorem OAI.KadisonKastler.real_combination_defect_lower line 41
  4. theorem OAI.KadisonKastler.ModularConjugationData.angled_projection_witness line 58