OAI/Analysis/Quantum/PPTSquare/ExplicitMaps.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExplicitPencil.M line 13
  2. def OAI.ExplicitPencil.pencil line 15
  3. def OAI.ExplicitPencil.L line 17
  4. lemma OAI.ExplicitPencil.data_symmetry line 26
  5. lemma OAI.ExplicitPencil.M_real line 28
  6. lemma OAI.ExplicitPencil.M_symmetry line 32
  7. lemma OAI.ExplicitPencil.L_apply line 37
  8. lemma OAI.ExplicitPencil.L_single line 39
  9. def OAI.ExplicitPencil.kraus line 42
  10. lemma OAI.ExplicitPencil.kraus_entry line 44
  11. lemma OAI.ExplicitPencil.L_eq_kraus line 48
  12. lemma OAI.ExplicitPencil.L_cp line 62
  13. lemma OAI.ExplicitPencil.transpose_L line 64
  14. lemma OAI.ExplicitPencil.L_ppt line 76