OAI/Analysis/Commutator/UnitaryMainTransport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.UnitaryTransport.algebra line 22
2. lemma OAI.Kadison.UnitaryTransport.mem_algebra line 31
3. lemma OAI.Kadison.UnitaryTransport.conj_norm line 39
4. lemma OAI.Kadison.UnitaryTransport.seminorm line 50
5. def OAI.Kadison.UnitaryTransport.copies line 69
6. lemma OAI.Kadison.UnitaryTransport.copies_apply line 73
7. lemma OAI.Kadison.UnitaryTransport.copies_symm_apply line 77
8. lemma OAI.Kadison.UnitaryTransport.diagonal line 80
9. lemma OAI.Kadison.UnitaryTransport.matrix line 87
10. lemma OAI.Kadison.UnitaryTransport.matrix_norm line 96
11. lemma OAI.Kadison.UnitaryTransport.matrix_commutator_norm line 100