OAI/Analysis/Commutator/FreeExpectation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.FreeExpectation.centered_mem line 122
2. lemma OAI.Kadison.FreeExpectation.centered_zero line 126
3. lemma OAI.Kadison.FreeExpectation.free_two line 130
4. lemma OAI.Kadison.FreeExpectation.free_three line 139
5. lemma OAI.Kadison.FreeExpectation.free_four line 151
6. lemma OAI.Kadison.FreeExpectation.centered_mul_zero line 165
7. lemma OAI.Kadison.FreeExpectation.mul_centered_zero line 172
8. lemma OAI.Kadison.FreeExpectation.centered_middle_pairing line 179
9. lemma OAI.Kadison.FreeExpectation.centered_sandwich_pairing line 189
10. theorem OAI.Kadison.FreeExpectation.free_compression_pairing line 199
11. def OAI.Kadison.FreeExpectation.factorSpace line 217
12. instance OAI.Kadison.FreeExpectation.(instance at line 222) line 222
13. lemma OAI.Kadison.FreeExpectation.vector_mem_factorSpace line 225
14. lemma OAI.Kadison.FreeExpectation.compression_error_orthogonal line 230
15. theorem OAI.Kadison.FreeExpectation.free_compression_projection line 249