OAI/Analysis/JiangSu/TraceCone/MatrixPositive.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TraceCone.matrixLimit_positive_approximation line 13
  2. theorem OAI.TraceCone.matrixLimit_cut_below_finite line 28
  3. def OAI.TraceCone.matrixPermute line 42
  4. theorem OAI.TraceCone.matrixPermute_entry line 46
  5. theorem OAI.TraceCone.positive_square_root line 52
  6. theorem OAI.TraceCone.matrixPermute_factorization line 57
  7. theorem OAI.TraceCone.matrixPermute_cuntzClass line 77
  8. theorem OAI.TraceCone.matrix_supported_permutation line 88
  9. theorem OAI.TraceCone.matrix_supported_cuntzClass line 111
  10. def OAI.TraceCone.matrixInterleaveRaw line 125
  11. lemma OAI.TraceCone.matrixInterleaveRaw_injective line 158
  12. def OAI.TraceCone.matrixInterleave line 171
  13. lemma OAI.TraceCone.matrixInterleave_injective line 174
  14. theorem OAI.TraceCone.matrixInterleave_isometry line 179
  15. theorem OAI.TraceCone.matrixInterleave_norm line 182
  16. theorem OAI.TraceCone.matrixInterleave_entry line 187