OAI/InformationTheory/DimensionTen/FiniteReadout.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Key rates for protocols with finite total terminal readouts.

  1. structure OAI.DimensionTen.AdmittedKeyTrial line 14
  2. def OAI.DimensionTen.AdmittedKeyTrial.actual line 33
  3. def OAI.DimensionTen.AdmittedKeyTrial.error line 36
  4. def OAI.DimensionTen.AdmittedKeyTrial.toCompleted line 38
  5. lemma OAI.DimensionTen.AdmittedKeyTrial.toCompleted_error line 49
  6. structure OAI.DimensionTen.AdmittedKeyScheme line 52
  7. def OAI.DimensionTen.AdmittedKeyScheme.Secure line 63
  8. def OAI.DimensionTen.AdmittedKeyScheme.lowerRate line 65
  9. def OAI.DimensionTen.AdmittedKeyScheme.toCompleted line 68
  10. lemma OAI.DimensionTen.AdmittedKeyScheme.toCompleted_secure line 72
  11. lemma OAI.DimensionTen.AdmittedKeyScheme.toCompleted_lowerRate line 74
  12. def OAI.DimensionTen.distillableSecretKey line 77
  13. lemma OAI.DimensionTen.distillableSecretKey_le_completed line 81
  14. lemma OAI.DimensionTen.distillableSecretKey_zero_of_inClass line 91