OAI/InformationTheory/SecretKey/Purification.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroKey.purification_filter_identity line 19
  2. def OAI.ZeroKey.BitDensity.mapReference line 42
  3. lemma OAI.ZeroKey.traceNorm_channel_sub line 52
  4. theorem OAI.ZeroKey.BitDensity.idealBitError_mapReference_le line 60
  5. lemma OAI.ZeroKey.BitProtocol.purifiedDensity_recovery line 127
  6. theorem OAI.ZeroKey.BitProtocol.uniform_gap_purification line 146
  7. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.FiniteReadout.postprocess_value line 208
  8. lemma OAI.ZeroKey.FiniteProtocol.canonicalOutput_ac line 257
  9. def OAI.ZeroKey.FiniteProtocol.outputDensity line 264
  10. def OAI.ZeroKey.FiniteProtocol.firstBit line 298
  11. lemma OAI.ZeroKey.FiniteProtocol.firstBit_completeReference line 301
  12. lemma OAI.ZeroKey.FiniteProtocol.firstBit_output_event line 317
  13. lemma OAI.ZeroKey.FiniteProtocol.firstBit_outputDensity line 333
  14. def OAI.ZeroKey.FiniteProtocol.secretKeyError line 382
  15. lemma OAI.ZeroKey.FiniteProtocol.secretKeyError_nonneg line 389
  16. theorem OAI.ZeroKey.FiniteProtocol.firstBit_error_le line 405
  17. theorem OAI.ZeroKey.FiniteProtocol.uniform_key_gap line 434
  18. def OAI.ZeroKey.FiniteProtocol.purifiedSecretKeyError line 475
  19. lemma OAI.ZeroKey.FiniteProtocol.firstBit_purifiedOutput_event line 492
  20. lemma OAI.ZeroKey.FiniteProtocol.firstBit_purifiedOutputDensity line 510
  21. theorem OAI.ZeroKey.FiniteProtocol.firstBit_purified_error_le line 531
  22. theorem OAI.ZeroKey.FiniteProtocol.uniform_purified_key_gap line 561
  23. lemma OAI.ZeroKey.KeyDensity.idealError_nonneg line 588
  24. lemma OAI.ZeroKey.KeyDensity.distance_nonneg line 590
  25. lemma OAI.ZeroKey.KeyDensity.distance_self line 593
  26. lemma OAI.ZeroKey.KeyDensity.idealError_triangle line 598
  27. theorem OAI.ZeroKey.KeyDensity.gap_of_traceNorm_limit line 604
  28. def OAI.ZeroKey.PositiveMatrixMeasure.toEveDensity line 617
  29. theorem OAI.ZeroKey.BitProtocol.uniform_gap_purification_dominated line 655
  30. theorem OAI.ZeroKey.FiniteProtocol.uniform_purified_key_gap_dominated line 685