OAI/Analysis/Pureness/Stabilization/MatrixSums.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzTrace.diagonalTwo line 12
  2. def OAI.CuntzTrace.coordinateTwo line 22
  3. lemma OAI.CuntzTrace.diagonalTwo_trace line 30
  4. def OAI.CuntzTrace.positivePair line 39
  5. def OAI.CuntzTrace.blockSum line 42
  6. lemma OAI.CuntzTrace.blockSum_rank line 45
  7. lemma OAI.CuntzTrace.sum_corner_cuntzBelow_blockSum line 51
  8. lemma OAI.CuntzTrace.rank_positive_add_le line 79
  9. lemma OAI.CuntzTrace.rank_abs_add_le line 84
  10. theorem OAI.CuntzTrace.sum_cut_rank line 96