OAI/Analysis/JiangSu/MatrixAlgebras/MatrixProjectionTests.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ConcreteMatrixUnits.projection_tests_control_entries line 16
2. structure OAI.DirectPacking.TracialMatrixModel line 46
3. def OAI.DirectPacking.MatrixPackingCertificate.compressLinear line 66
4. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_zero line 72
5. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_sum_diag line 74
6. def OAI.DirectPacking.MatrixPackingCertificate.commutatorLinear line 78
7. lemma OAI.DirectPacking.MatrixPackingCertificate.entry_commutator_bound line 83
8. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_unit_bound line 98
9. lemma OAI.DirectPacking.matrix_models_from_packing line 107