OAI/InformationTheory/Entanglement/ProjectionData.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ProjectionCriterion.correlation line 13
  2. structure OAI.ProjectionCriterion.Data line 15
  3. def OAI.ProjectionCriterion.Data.c line 34
  4. def OAI.ProjectionCriterion.Data.H line 35
  5. def OAI.ProjectionCriterion.Data.Psi line 36
  6. def OAI.ProjectionCriterion.Data.C line 40
  7. def OAI.ProjectionCriterion.Data.B line 41
  8. lemma OAI.ProjectionCriterion.Data.c_symm line 44
  9. lemma OAI.ProjectionCriterion.Data.c_self line 47
  10. lemma OAI.ProjectionCriterion.Data.P_psd line 49
  11. lemma OAI.ProjectionCriterion.Data.H_self line 53
  12. lemma OAI.ProjectionCriterion.Data.H_symm line 55
  13. lemma OAI.ProjectionCriterion.Data.H_adjoint line 60
  14. lemma OAI.ProjectionCriterion.Data.H_hermitian line 64
  15. lemma OAI.ProjectionCriterion.Data.Psi_single line 66
  16. lemma OAI.ProjectionCriterion.Data.choi_Psi line 68
  17. def OAI.ProjectionCriterion.Data.gramFactor line 72
  18. lemma OAI.ProjectionCriterion.Data.choi_gram line 74
  19. lemma OAI.ProjectionCriterion.Data.Psi_cp line 90
  20. lemma OAI.ProjectionCriterion.Data.Psi_input_transpose line 95
  21. lemma OAI.ProjectionCriterion.Data.Psi_ppt line 105
  22. lemma OAI.ProjectionCriterion.Data.adjoint_ppt line 109
  23. lemma OAI.ProjectionCriterion.Data.adjoint_output_transpose line 110