OAI/InformationTheory/Entanglement/ProjectionRealMain.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ProjectionCriterion.projector_real_smul line 11
2. def OAI.ProjectionCriterion.Phi line 18
3. lemma OAI.ProjectionCriterion.Phi_projector line 19
4. lemma OAI.ProjectionCriterion.Data.localChannel_input_transpose line 28
5. lemma OAI.ProjectionCriterion.Data.rho_identification line 34
6. lemma OAI.ProjectionCriterion.Data.rho_represented line 46
7. theorem OAI.ProjectionCriterion.real_channel line 53