OAI/Analysis/TracialSplitting/ScalarCompression.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentMain.spectralAtom_ne_zero line 22
2. structure OAI.CurrentMain.ProjectionPartition line 32
3. lemma OAI.CurrentMain.ProjectionPartition.mul_parent line 47
4. lemma OAI.CurrentMain.ProjectionPartition.parent_mul line 58
5. lemma OAI.CurrentMain.ProjectionPartition.piece_le line 69
6. lemma OAI.CurrentMain.norm_compress_le line 75
7. lemma OAI.CurrentMain.compression_persist line 84
8. def OAI.CurrentMain.cornerSpectralPartition line 94
9. lemma OAI.CurrentMain.scalarCompression_selfAdjoint line 114
10. def OAI.CurrentMain.ProjectionPartition.refine line 150
11. def OAI.CurrentMain.ProjectionPartition.empty line 172
12. def OAI.CurrentMain.ProjectionPartition.singleton line 180
13. lemma OAI.CurrentMain.scalarCompressions_selfAdjoint line 190
14. lemma OAI.CurrentMain.scalar_compressions line 217
15. instance OAI.CurrentMain.ProjectionCorner.(instance at line 254) line 254
16. lemma OAI.CurrentMain.ProjectionCorner.coe_nonneg_iff line 281
17. lemma OAI.CurrentMain.ProjectionCorner.coe_le_iff line 284
18. lemma OAI.CurrentMain.ProjectionCorner.compress_nonneg line 286
19. def OAI.CurrentMain.spectralThreshold line 298
20. lemma OAI.CurrentMain.spectralThreshold_projection line 301
21. lemma OAI.CurrentMain.spectralThreshold_complement line 311
22. lemma OAI.CurrentMain.spectralThreshold_lower line 323
23. lemma OAI.CurrentMain.spectralThreshold_complement_upper line 338
24. lemma OAI.CurrentMain.compress_perturbation_lower line 354
25. lemma OAI.CurrentMain.compress_perturbation_upper line 362