OAI/Analysis/KadisonKastler/MatrixCentralCorner.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The Hilbert-space identification of a matrix corner and central vectors

The map from Haagerup's Lemma3.5 is a genuine unitary between these closed subspaces. State and natural-cone properties are separate claims.

  1. theorem OAI.KadisonKastler.starProjection_range_of_projection line 21
  2. def OAI.KadisonKastler.matrixCentralCornerProjection line 38
  3. theorem OAI.KadisonKastler.matrixCentralCornerProjection_isProjection line 43
  4. def OAI.KadisonKastler.matrixCentralCorner line 59
  5. theorem OAI.KadisonKastler.matrixCentralCorner_complete line 64
  6. def OAI.KadisonKastler.matrixCentralColumn line 69
  7. theorem OAI.KadisonKastler.matrixCentralColumn_initial line 74
  8. theorem OAI.KadisonKastler.matrixCentralColumn_final line 83
  9. def OAI.KadisonKastler.matrixCentralCornerEquiv line 93