OAI/InformationTheory/Entanglement/HilbertMeasure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SecretKey.PositiveHilbertMeasure line 15
  2. def OAI.SecretKey.PositiveHilbertMeasure.compress line 28
  3. lemma OAI.SecretKey.PositiveHilbertMeasure.compress_value line 36
  4. def OAI.SecretKey.PositiveHilbertMeasure.traceComplex line 40
  5. lemma OAI.SecretKey.PositiveHilbertMeasure.traceComplex_value line 41
  6. lemma OAI.SecretKey.PositiveHilbertMeasure.erased_entries line 48
  7. def OAI.SecretKey.PositiveHilbertMeasure.erase line 66
  8. lemma OAI.SecretKey.PositiveHilbertMeasure.erase_value line 72
  9. lemma OAI.SecretKey.PositiveHilbertMeasure.erase_traceMeasure line 76
  10. theorem OAI.SecretKey.PositiveHilbertMeasure.erase_law line 85