OAI/Analysis/JiangSu/TraceCone/CompactOperators.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TraceCone.rankOneGenerators line 13
  2. def OAI.TraceCone.finiteRankAlgebra line 15
  3. def OAI.TraceCone.compactOperatorAlgebra line 18
  4. instance OAI.TraceCone.compactOperatorAlgebra_closed line 21
  5. abbrev OAI.TraceCone.CompactOperators line 24
  6. instance OAI.TraceCone.(instance at line 26) line 26
  7. lemma OAI.TraceCone.rankOne_isCompact line 31
  8. lemma OAI.TraceCone.finiteRankAlgebra_compact line 36
  9. theorem OAI.TraceCone.compactOperators_areCompact line 55
  10. theorem OAI.TraceCone.rankOne_mem_compactOperators line 61
  11. abbrev OAI.TraceCone.StandardHilbert line 65
  12. abbrev OAI.TraceCone.StandardCompacts line 67
  13. def OAI.TraceCone.standardVector line 77
  14. lemma OAI.TraceCone.inner_standardVector line 78
  15. lemma OAI.TraceCone.norm_standardVector line 81
  16. def OAI.TraceCone.compactMatrixUnit line 84
  17. theorem OAI.TraceCone.compactMatrixUnit_star line 87
  18. theorem OAI.TraceCone.compactMatrixUnit_mul line 92
  19. theorem OAI.TraceCone.compactMatrixUnit_norm line 100
  20. def OAI.TraceCone.compactProjection line 104
  21. lemma OAI.TraceCone.compactProjection_star line 106
  22. lemma OAI.TraceCone.compactProjection_mul line 108
  23. theorem OAI.TraceCone.compactProjection_compress line 113