OAI/InformationTheory/Entanglement/ProbePOVM.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecretKey.testSum line 15
  2. lemma OAI.SecretKey.testSum_psd line 17
  3. def OAI.SecretKey.probeScale line 19
  4. lemma OAI.SecretKey.probeScale_pos line 21
  5. lemma OAI.SecretKey.probeScale_mul_trace line 25
  6. def OAI.SecretKey.probePOVM line 30
  7. lemma OAI.SecretKey.probePOVM_psd line 33
  8. lemma OAI.SecretKey.probePOVM_sum line 51
  9. lemma OAI.SecretKey.linear_eq_zero_of_probePOVM line 55
  10. theorem OAI.SecretKey.tensor_product_of_probePOVM line 64