OAI/Analysis/JiangSu/Traceless/TracelessCanonicalPure.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentMain.Traceless.CanonicalStabilization line 16
2. instance OAI.CurrentMain.Traceless.(instance at line 19) line 19
3. instance OAI.CurrentMain.Traceless.(instance at line 23) line 23
4. instance OAI.CurrentMain.Traceless.(instance at line 26) line 26
5. def OAI.CurrentMain.Traceless.EmptyTraceComparison line 29
6. def OAI.CurrentMain.Traceless.PurelyInfinite line 32
7. theorem OAI.CurrentMain.Traceless.pure_infiniteness_of_empty_trace_comparison line 36
8. theorem OAI.CurrentMain.Traceless.unit_cuntz_of_empty_comparison line 66
9. lemma OAI.CurrentMain.Traceless.isometry_norm_one line 81
10. lemma OAI.CurrentMain.Traceless.orthogonal_isometries_of_ranges line 87
11. theorem OAI.CurrentMain.Traceless.exists_two_isometries line 96
12. theorem OAI.CurrentMain.Traceless.finite_isometries_of_two line 116
13. lemma OAI.CurrentMain.Traceless.high_cut_ne_zero line 153
14. lemma OAI.CurrentMain.Traceless.isometry_peak_bound line 163
15. lemma OAI.CurrentMain.Traceless.cross_compression_bound line 196