OAI/InformationTheory/Entanglement/ProjectionReal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ProjectionCriterion.Data.RealProjections line 16
  2. lemma OAI.ProjectionCriterion.Data.P_transpose line 18
  3. lemma OAI.ProjectionCriterion.Data.H_transpose line 24
  4. lemma OAI.ProjectionCriterion.Data.adjoint_input_transpose line 30
  5. lemma OAI.ProjectionCriterion.Data.adjoint_trace line 37
  6. lemma OAI.ProjectionCriterion.Data.choi_real line 44
  7. def OAI.ProjectionCriterion.Data.localChannel line 52
  8. def OAI.ProjectionCriterion.Data.rho line 53
  9. lemma OAI.ProjectionCriterion.Data.localChannel_ppt line 56
  10. lemma OAI.ProjectionCriterion.Data.localChannel_tp line 61
  11. lemma OAI.ProjectionCriterion.Data.rho_psd line 70
  12. lemma OAI.ProjectionCriterion.Data.rho_trace line 76
  13. lemma OAI.ProjectionCriterion.Data.separable_scaling line 84
  14. lemma OAI.ProjectionCriterion.Data.rho_nonseparable line 89