OAI/Analysis/JiangSu/TraceCone/MatrixEntries.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TraceCone.matrixInclusion_entry_inside line 14
  2. theorem OAI.TraceCone.matrixInclusion_entry_outside line 24
  3. theorem OAI.TraceCone.matrixInclusion_entry line 46
  4. lemma OAI.TraceCone.finProdFinEquiv_cast line 54
  5. theorem OAI.TraceCone.matrixInterleave_inclusion line 58
  6. def OAI.TraceCone.matrixLimitBlock line 87
  7. theorem OAI.TraceCone.matrixLimitBlock_norm line 90
  8. theorem OAI.TraceCone.matrixLimitBlock_compatible line 95
  9. lemma OAI.TraceCone.le_double line 100
  10. def OAI.TraceCone.matrixTripleLeftIndex line 102
  11. def OAI.TraceCone.matrixTripleRightIndex line 107
  12. lemma OAI.TraceCone.matrixTripleLeftIndex_injective line 112
  13. lemma OAI.TraceCone.matrixTripleRightIndex_injective line 119
  14. def OAI.TraceCone.matrixTripleLeft line 126
  15. def OAI.TraceCone.matrixTripleRight line 129
  16. lemma OAI.TraceCone.matrixTriple_entries line 132
  17. lemma OAI.TraceCone.matrixTripleLeft_outside line 141
  18. lemma OAI.TraceCone.matrixTripleRight_outside line 162
  19. theorem OAI.TraceCone.matrixTriple_permutation line 183