OAI/InformationTheory/Entanglement/InformationalComplete.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.projector_polarization line 13
  2. def OAI.SecretKey.testBasis line 25
  3. lemma OAI.SecretKey.star_testBasis line 27
  4. lemma OAI.SecretKey.single_projector_polarization line 31
  5. theorem OAI.SecretKey.linear_eq_zero_of_projector_tests line 40
  6. abbrev OAI.SecretKey.PositiveTestIndex line 58
  7. def OAI.SecretKey.positiveTestVector line 59
  8. def OAI.SecretKey.positiveTest line 63
  9. lemma OAI.SecretKey.positiveTest_psd line 64
  10. lemma OAI.SecretKey.linear_eq_zero_of_positive_tests line 66
  11. def OAI.SecretKey.tensorTraceDifference line 73
  12. theorem OAI.SecretKey.tensor_product_of_positive_tests line 101