OAI/Analysis/Commutator/PaulsenPositive.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.Paulsen.IsCompletelyContractive line 27
2. def OAI.Kadison.Paulsen.MatrixTest.leftDiagonal line 36
3. def OAI.Kadison.Paulsen.MatrixTest.rightDiagonal line 39
4. def OAI.Kadison.Paulsen.MatrixTest.offDiagonal line 42
5. lemma OAI.Kadison.Paulsen.MatrixTest.lower_entry line 46
6. lemma OAI.Kadison.Paulsen.MatrixTest.source_block line 51
7. lemma OAI.Kadison.Paulsen.MatrixTest.output_block line 64
8. lemma OAI.Kadison.Paulsen.MatrixTest.source_nonneg line 77
9. lemma OAI.Kadison.Paulsen.MatrixTest.diagonal_nonneg_pair line 83
10. lemma OAI.Kadison.Paulsen.MatrixTest.target_nonneg line 99
11. lemma OAI.Kadison.Paulsen.MatrixTest.output_nonneg line 112
12. theorem OAI.Kadison.Paulsen.systemMap_completelyPositive line 121