OAI/Analysis/KadisonKastler/PairedMatrixProjection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The projection associated with two commuting matrix actions

This is the finite-matrix formula for Haagerup's central-vector projection: the normalized sum of matching left and conjugate-right matrix units.

  1. def OAI.KadisonKastler.pairedMatrixProjection line 22
  2. theorem OAI.KadisonKastler.pairedMatrixSum_left line 26
  3. theorem OAI.KadisonKastler.pairedMatrixSum_right line 33
  4. theorem OAI.KadisonKastler.pairedMatrixProjection_intertwines line 45
  5. theorem OAI.KadisonKastler.pairedMatrixProjection_selfAdjoint line 52
  6. theorem OAI.KadisonKastler.pairedMatrixProjection_fixed line 66