OAI/Analysis/JiangSu/MatrixAlgebras/CornerCompression.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Pureness.cornerProjection_star line 17
  2. lemma OAI.Pureness.cornerProjection_norm_le line 23
  3. theorem OAI.Pureness.compress_norm_le line 30
  4. theorem OAI.Pureness.corner_compress_cuntz line 41
  5. def OAI.Pureness.scalarMatrixHom line 58
  6. def OAI.Pureness.singleMatrix line 67
  7. lemma OAI.Pureness.singleMatrix_mul_same line 71
  8. lemma OAI.Pureness.singleMatrix_mul_ne line 79
  9. lemma OAI.Pureness.matrix_eq_sum_single line 89
  10. lemma OAI.Pureness.trace_single_offDiagonal line 96
  11. lemma OAI.Pureness.trace_single_diagonal_eq line 103
  12. lemma OAI.Pureness.trace_matrix_eq_sum_diagonal line 108
  13. lemma OAI.Pureness.scalarMatrix_eq_sum_single line 122
  14. lemma OAI.Pureness.trace_scalarMatrix line 129
  15. theorem OAI.Pureness.matrixTrace_comap_scale line 136
  16. lemma OAI.Pureness.TracialState.ext line 148
  17. theorem OAI.Pureness.matrixTracialState_comap line 155
  18. theorem OAI.Pureness.comap_matrixTracialState line 163
  19. theorem OAI.Pureness.matrix_tracialState_nonempty_iff line 174