OAI/Analysis/JiangSu/TraceCone/MatrixEmbedding.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TraceCone.matrixEmbedding_size line 14
  2. def OAI.TraceCone.matrixEmbeddingPermutation line 17
  3. lemma OAI.TraceCone.matrixEmbeddingPermutation_apply line 21
  4. def OAI.TraceCone.matrixEmbedding line 26
  5. theorem OAI.TraceCone.matrixEmbedding_entry line 29
  6. theorem OAI.TraceCone.matrixEmbedding_outside line 35
  7. theorem OAI.TraceCone.matrixEmbedding_ext line 49
  8. theorem OAI.TraceCone.matrixEmbedding_cuntzClass line 62
  9. def OAI.TraceCone.matrixPairLeft line 86
  10. def OAI.TraceCone.matrixPairRight line 94
  11. def OAI.TraceCone.matrixEvenStage line 102
  12. def OAI.TraceCone.matrixOddStage line 104
  13. lemma OAI.TraceCone.matrixEvenStage_compatible line 107
  14. lemma OAI.TraceCone.matrixOddStage_compatible line 110
  15. def OAI.TraceCone.matrixEven line 114
  16. def OAI.TraceCone.matrixOdd line 115
  17. lemma OAI.TraceCone.matrixEven_stage line 117
  18. lemma OAI.TraceCone.matrixOdd_stage line 119
  19. theorem OAI.TraceCone.matrixEven_mul_matrixOdd line 122
  20. theorem OAI.TraceCone.matrixOdd_mul_matrixEven line 146
  21. def OAI.TraceCone.matrixBlockHom line 150
  22. def OAI.TraceCone.positiveProduct line 171
  23. theorem OAI.TraceCone.positiveProduct_cuntzBelow line 174
  24. def OAI.TraceCone.matrixBlockPositive line 183
  25. theorem OAI.TraceCone.matrixBlockPositive_cuntzBelow line 186
  26. def OAI.TraceCone.CuntzClass.matrixAdd line 193
  27. lemma OAI.TraceCone.CuntzClass.matrixAdd_mk line 200
  28. theorem OAI.TraceCone.CuntzClass.matrixAdd_mono line 203