OAI/Analysis/Pureness/Stabilization/CompactDensity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CuntzTrace.StandardOperators line 9
2. def OAI.CuntzTrace.matrixUnitGenerators line 14
3. def OAI.CuntzTrace.matrixUnitAlgebra line 17
4. lemma OAI.CuntzTrace.single_eq_smul_standardVector line 20
5. lemma OAI.CuntzTrace.rankOne_single_single line 25
6. def OAI.CuntzTrace.standardPartialVector line 32
7. lemma OAI.CuntzTrace.standardPartialVector_tendsto line 35
8. lemma OAI.CuntzTrace.single_rankOne_mem_matrixUnitClosure line 39
9. lemma OAI.CuntzTrace.rankOne_right_partial_tendsto line 46
10. lemma OAI.CuntzTrace.leftSingle_rankOne_mem_matrixUnitClosure line 52
11. theorem OAI.CuntzTrace.rankOne_mem_matrixUnitClosure line 61
12. theorem OAI.CuntzTrace.matrixUnitClosure_eq_compactOperatorAlgebra line 73