OAI/Analysis/Commutator/AlgebraFreeExpectation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.AlgebraFreeExpectation.centered_mem line 22
2. lemma OAI.Kadison.AlgebraFreeExpectation.centered_zero line 28
3. lemma OAI.Kadison.AlgebraFreeExpectation.free_two line 32
4. lemma OAI.Kadison.AlgebraFreeExpectation.free_three line 41
5. lemma OAI.Kadison.AlgebraFreeExpectation.free_four line 53
6. lemma OAI.Kadison.AlgebraFreeExpectation.centered_mul_zero line 67
7. lemma OAI.Kadison.AlgebraFreeExpectation.mul_centered_zero line 74
8. lemma OAI.Kadison.AlgebraFreeExpectation.centered_middle_pairing line 81
9. lemma OAI.Kadison.AlgebraFreeExpectation.centered_sandwich_pairing line 91
10. theorem OAI.Kadison.AlgebraFreeExpectation.free_compression_pairing line 101