OAI/InformationTheory/SecretKey/KeyRate.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroKey.card_keyWord line 15
  2. def OAI.ZeroKey.commonPublicLaw line 34
  3. lemma OAI.ZeroKey.commonPublicLaw_univ line 37
  4. instance OAI.ZeroKey.commonPublicLaw_finite line 43
  5. lemma OAI.ZeroKey.absolutelyContinuous_commonPublicLaw line 46
  6. lemma OAI.ZeroKey.KeyImplementation.uniform_gap line 73
  7. lemma OAI.ZeroKey.IsCompletedKeyOutput.of_implementation line 89
  8. theorem OAI.ZeroKey.IsCompletedKeyOutput.uniform_gap line 97
  9. lemma OAI.ZeroKey.CompletedKeyTrial.error_nonneg line 115
  10. lemma OAI.ZeroKey.CompletedKeyTrial.uniform_error line 117
  11. def OAI.ZeroKey.groupVector line 128
  12. lemma OAI.ZeroKey.outer_groupVector line 132
  13. lemma OAI.ZeroKey.tensorMap_kronecker line 138
  14. lemma OAI.ZeroKey.matrixUnit_finProd line 153
  15. lemma OAI.ZeroKey.tensorLinear_unit line 170
  16. lemma OAI.ZeroKey.tensorMap_groupTensor line 181
  17. lemma OAI.ZeroKey.InClass.groupTensor line 212
  18. lemma OAI.ZeroKey.InClass.positiveCopies line 222
  19. lemma OAI.ZeroKey.CompletedKeyScheme.eventually_length_zero line 245
  20. lemma OAI.ZeroKey.CompletedKeyScheme.lowerRate_zero line 253
  21. theorem OAI.ZeroKey.class_distillableSecretKey_zero line 263