OAI/Analysis/KadisonKastler/UnitaryResidualGap.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Near-central unitaries with a uniform residual gap

The scalar hull conclusion of Haagerup's Proposition 1.3 gives the unitary gap in Lemma 3.2. Centered cyclic approximation extends the operator-vector calculation to every vector orthogonal to the reference.

  1. theorem OAI.KadisonKastler.centered_unitary_gap line 25
  2. theorem OAI.KadisonKastler.exists_unitary_residual_gap_of_state_defect_bound line 59
  3. theorem OAI.KadisonKastler.exists_unitary_residual_gap_of_scalar_state_hulls line 96