OAI/Analysis/Commutator/ChoiRecovery.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.OperatorSystem.choiEmbedding line 25
2. lemma OAI.Kadison.OperatorSystem.choiEmbedding_apply line 31
3. lemma OAI.Kadison.OperatorSystem.choiEmbedding_basis line 34
4. def OAI.Kadison.OperatorSystem.choiRepresentation line 38
5. lemma OAI.Kadison.OperatorSystem.choi_coefficient line 41
6. lemma OAI.Kadison.OperatorSystem.entry_mem line 49
7. def OAI.Kadison.OperatorSystem.systemEntry line 53
8. lemma OAI.Kadison.OperatorSystem.mapMatrix_systemEntry line 57
9. lemma OAI.Kadison.OperatorSystem.choi_systemEntry line 71
10. lemma OAI.Kadison.OperatorSystem.sum_basis line 82
11. lemma OAI.Kadison.OperatorSystem.basis_inner_ext line 86