OAI/Analysis/Pureness/Operators/CompressionCompatibility.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.compress_nonneg line 12
2. lemma OAI.CuntzPureness.matrixRank_compress_le line 18
3. lemma OAI.CuntzPureness.matrixTrace_compress_le line 26
4. lemma OAI.CuntzPureness.completedCompress_nonneg line 36
5. lemma OAI.CuntzPureness.completedProjection_mul_le line 43
6. lemma OAI.CuntzPureness.completedProjection_mul_ge line 49
7. lemma OAI.CuntzPureness.completedCornerCut_nested line 55
8. lemma OAI.CuntzPureness.completedCornerCut_include line 63
9. theorem OAI.CuntzPureness.completedCompress_compat line 68
10. lemma OAI.CuntzPureness.completedCompression_trace_monotone line 74
11. lemma OAI.CuntzPureness.completedCompression_rank_monotone line 81