OAI/Analysis/JiangSu/TraceCone/CompactDensity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TraceCone.StandardOperators line 15
  2. def OAI.TraceCone.matrixUnitGenerators line 21
  3. def OAI.TraceCone.matrixUnitAlgebra line 24
  4. lemma OAI.TraceCone.single_eq_smul_standardVector line 27
  5. lemma OAI.TraceCone.rankOne_single_single line 32
  6. def OAI.TraceCone.standardPartialVector line 39
  7. lemma OAI.TraceCone.standardPartialVector_tendsto line 42
  8. lemma OAI.TraceCone.single_rankOne_mem_matrixUnitClosure line 46
  9. lemma OAI.TraceCone.rankOne_right_partial_tendsto line 53
  10. lemma OAI.TraceCone.leftSingle_rankOne_mem_matrixUnitClosure line 59
  11. theorem OAI.TraceCone.rankOne_mem_matrixUnitClosure line 68
  12. theorem OAI.TraceCone.matrixUnitClosure_eq_compactOperatorAlgebra line 80