OAI/Analysis/Quantum/DimensionTen/Channel.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

A trace-preserving PPT channel with an entangled square, from the dimension-ten pair.

  1. def OAI.DimensionTen.phiOneLinear line 15
  2. lemma OAI.DimensionTen.phiOneLinear_apply line 18
  3. lemma OAI.DimensionTen.phiTwoLinear_apply line 22
  4. lemma OAI.DimensionTen.phiOneLinear_cp line 24
  5. lemma OAI.DimensionTen.phiTwoLinear_cp line 27
  6. lemma OAI.DimensionTen.phiOneLinear_ppt line 37
  7. lemma OAI.DimensionTen.phiTwoLinear_ppt line 46
  8. lemma OAI.DimensionTen.linear_composite_choi line 55
  9. lemma OAI.DimensionTen.linear_composite_not_separable line 61
  10. def OAI.DimensionTen.channel line 69
  11. def OAI.DimensionTen.channel21 line 73
  12. def OAI.DimensionTen.PublishedChoi21 line 76
  13. lemma OAI.DimensionTen.channel_choi_corner line 80
  14. theorem OAI.DimensionTen.main_channel_conditional line 88
  15. theorem OAI.DimensionTen.main_channel_fin21_conditional line 109
  16. theorem OAI.DimensionTen.publishedChoi21 line 126
  17. theorem OAI.DimensionTen.main_channel line 130
  18. theorem OAI.DimensionTen.main_channel_fin21 line 135
  19. theorem OAI.DimensionTen.exists_channel_fin21 line 140

    Distinct definitions of this name: ComparatorChallenges/DimensionTenChannel.lean:45 (same statement text; different proof or body). Qualify references as OAI.DimensionTen.exists_channel_fin21@path.