OAI/Analysis/Quantum/PPTSquare/TensorPositivity.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TensorCriterion.cp_sum line 15
  2. lemma OAI.TensorCriterion.ad_single_apply line 28
  3. lemma OAI.TensorCriterion.cp_of_choi line 39
  4. lemma OAI.TensorCriterion.choi_simultaneous_transpose line 66
  5. lemma OAI.TensorCriterion.cp_simultaneous_transpose line 71
  6. lemma OAI.TensorCriterion.ppt_input_transpose line 77
  7. lemma OAI.TensorCriterion.hsAdjoint_single line 82
  8. lemma OAI.TensorCriterion.choi_hsAdjoint line 86
  9. lemma OAI.TensorCriterion.cp_hsAdjoint line 93
  10. lemma OAI.TensorCriterion.hsAdjoint_input_transpose line 99
  11. lemma OAI.TensorCriterion.ppt_hsAdjoint line 104
  12. lemma OAI.TensorCriterion.tensorMap_kronecker line 118
  13. lemma OAI.TensorCriterion.choi_tensorMap line 131
  14. lemma OAI.TensorCriterion.cp_tensorMap line 143
  15. lemma OAI.TensorCriterion.transpose_tensorMap line 149
  16. lemma OAI.TensorCriterion.ppt_tensorMap line 153
  17. lemma OAI.TensorCriterion.ppt_comp_cp line 160
  18. lemma OAI.TensorCriterion.transpose_ad_comp line 167
  19. lemma OAI.TensorCriterion.ppt_ad_comp line 176
  20. lemma OAI.TensorCriterion.ppt_output_transpose line 182
  21. lemma OAI.TensorCriterion.S_ppt line 185
  22. lemma OAI.TensorCriterion.R_ppt line 189
  23. lemma OAI.TensorCriterion.Phi1_ppt line 192
  24. lemma OAI.TensorCriterion.Phi2_ppt line 195
  25. lemma OAI.TensorCriterion.cp_positive line 199
  26. lemma OAI.TensorCriterion.trace_hsAdjoint line 204