OAI/Analysis/Quantum/PPTSquare/ChannelModel.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ChannelCompletion.Mat line 17

    Also declared: ComparatorChallenges/DimensionTenChannel.lean:11 (same declaration text).

  2. abbrev OAI.ChannelCompletion.Map line 18

    Also declared: ComparatorChallenges/DimensionTenChannel.lean:12 (same declaration text).

  3. def OAI.ChannelCompletion.amplify line 22

    Also declared: ComparatorChallenges/DimensionTenChannel.lean:16 (same declaration text).

  4. def OAI.ChannelCompletion.choi line 25
  5. def OAI.ChannelCompletion.CP line 28

    Also declared: ComparatorChallenges/DimensionTenChannel.lean:19 (same declaration text).

  6. def OAI.ChannelCompletion.transposeMap line 31

    Also declared: ComparatorChallenges/DimensionTenChannel.lean:22 (same declaration text).

  7. def OAI.ChannelCompletion.PPT line 36

    Also declared: ComparatorChallenges/DimensionTenChannel.lean:27 (same declaration text).

  8. def OAI.ChannelCompletion.TracePreserving line 38

    Also declared: ComparatorChallenges/DimensionTenChannel.lean:29 (same declaration text).

  9. def OAI.ChannelCompletion.Separable line 40

    Also declared: ComparatorChallenges/DimensionTenChannel.lean:31 (same declaration text).

  10. def OAI.ChannelCompletion.EntanglementBreaking line 45

    Also declared: ComparatorChallenges/DimensionTenChannel.lean:36 (same declaration text).

  11. def OAI.ChannelCompletion.ad line 49
  12. def OAI.ChannelCompletion.effect line 54
  13. def OAI.ChannelCompletion.coefficient line 57
  14. def OAI.ChannelCompletion.defect line 60
  15. abbrev OAI.ChannelCompletion.Space line 63
  16. def OAI.ChannelCompletion.first line 65
  17. def OAI.ChannelCompletion.second line 66
  18. def OAI.ChannelCompletion.flag line 67
  19. def OAI.ChannelCompletion.coord line 69
  20. def OAI.ChannelCompletion.W0 line 72
  21. def OAI.ChannelCompletion.W1 line 73
  22. def OAI.ChannelCompletion.flagProjection line 74
  23. def OAI.ChannelCompletion.theta line 76
  24. theorem OAI.ChannelCompletion.ad_apply line 100
  25. theorem OAI.ChannelCompletion.transposeMap_apply line 102
  26. lemma OAI.ChannelCompletion.amplify_ad line 105
  27. lemma OAI.ChannelCompletion.cp_ad line 117
  28. lemma OAI.ChannelCompletion.cp_comp line 124
  29. lemma OAI.ChannelCompletion.cp_add line 129
  30. lemma OAI.ChannelCompletion.cp_smul line 134
  31. def OAI.ChannelCompletion.omega line 139
  32. lemma OAI.ChannelCompletion.amplify_omega line 142
  33. lemma OAI.ChannelCompletion.cp_choi line 152
  34. lemma OAI.ChannelCompletion.eb_choi line 157
  35. lemma OAI.ChannelCompletion.effect_eq_sum line 163
  36. lemma OAI.ChannelCompletion.effect_psd line 168
  37. lemma OAI.ChannelCompletion.effect_trace line 172
  38. lemma OAI.ChannelCompletion.coefficient_pos line 186