OAI/Analysis/KadisonKastler/MatrixDiagonalAverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The two-term diagonal average in Cuntz coordinates

  1. theorem OAI.KadisonKastler.CuntzFamily.matrix_conjugate_liftedTwoBlockUnitary line 17
  2. theorem OAI.KadisonKastler.CuntzFamily.matrix_diagonal_average line 27
  3. theorem OAI.KadisonKastler.CuntzFamily.exists_diagonal_average_mem line 46