OAI/Analysis/Commutator/MatrixExpectation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.MatrixExpectation.expectation line 22
2. lemma OAI.Kadison.MatrixExpectation.expectation_apply line 26
3. lemma OAI.Kadison.MatrixExpectation.star_expectation line 31
4. lemma OAI.Kadison.MatrixExpectation.selfAdjoint line 36
5. lemma OAI.Kadison.MatrixExpectation.single_left line 40
6. lemma OAI.Kadison.MatrixExpectation.single_right line 53
7. lemma OAI.Kadison.MatrixExpectation.commutes line 66
8. lemma OAI.Kadison.MatrixExpectation.matrixSandwich line 77
9. lemma OAI.Kadison.MatrixExpectation.matrixSum line 87
10. lemma OAI.Kadison.MatrixExpectation.on_matrix line 92
11. lemma OAI.Kadison.MatrixExpectation.card_ne line 101
12. lemma OAI.Kadison.MatrixExpectation.fixes line 103
13. lemma OAI.Kadison.MatrixExpectation.idempotent line 113
14. lemma OAI.Kadison.MatrixExpectation.inner_symm line 122
15. lemma OAI.Kadison.MatrixExpectation.norm_vector_le line 140
16. lemma OAI.Kadison.MatrixExpectation.trace_preserving line 150
17. lemma OAI.Kadison.MatrixExpectation.on_matrix_trace line 157