OAI/Analysis/Commutator/IntertwinerCompression.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.IntertwinerCompression.transfer line 30
2. lemma OAI.Kadison.IntertwinerCompression.adjoint_intertwines line 34
3. lemma OAI.Kadison.IntertwinerCompression.transfer_left line 38
4. lemma OAI.Kadison.IntertwinerCompression.transfer_right line 43
5. lemma OAI.Kadison.IntertwinerCompression.transfer_sub line 50
6. lemma OAI.Kadison.IntertwinerCompression.transfer_norm_le line 53
7. lemma OAI.Kadison.IntertwinerCompression.transfer_commutator line 64
8. lemma OAI.Kadison.IntertwinerCompression.transfer_commutator_norm_le line 68
9. lemma OAI.Kadison.IntertwinerCompression.amplify_intertwines line 75
10. lemma OAI.Kadison.IntertwinerCompression.amplify_transfer line 91