OAI/InformationTheory/Entanglement/FiniteInputInstrument.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SecretKey.FiniteInputInstrument line 15
  2. def OAI.SecretKey.FiniteInputInstrument.referenceLaw line 23
  3. def OAI.SecretKey.FiniteInputInstrument.purificationLaw line 27
  4. def OAI.SecretKey.FiniteInputInstrument.rawProbe line 30
  5. lemma OAI.SecretKey.FiniteInputInstrument.rawProbe_entry line 32
  6. lemma OAI.SecretKey.FiniteInputInstrument.law_entries line 35
  7. theorem OAI.SecretKey.FiniteInputInstrument.purificationLaw_eq_filter line 42
  8. lemma OAI.SecretKey.FiniteInputInstrument.purificationLaw_total line 51
  9. lemma OAI.SecretKey.FiniteInputInstrument.rawProbe_total line 57
  10. theorem OAI.SecretKey.FiniteInputInstrument.rawProbe_test line 65
  11. theorem OAI.SecretKey.FiniteInputInstrument.referenceLaw_conjugation line 74