OAI/InformationTheory/SecretKey/Sampling.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UnrestrictedQuantum.filterFunctional line 20
  2. theorem OAI.UnrestrictedQuantum.filter_precompose line 28
  3. theorem OAI.UnrestrictedQuantum.filter_precompose_two line 33
  4. lemma OAI.UnrestrictedQuantum.filter_positive line 39
  5. theorem OAI.UnrestrictedQuantum.InstrumentRun.event_reference line 55
  6. theorem OAI.UnrestrictedQuantum.InstrumentRun.filter_event line 62
  7. theorem OAI.ZeroKey.sample_instrument_update line 87
  8. lemma OAI.ZeroKey.uniform_prefix_fresh_independent line 102
  9. lemma OAI.ZeroKey.uniform_tape_eval line 114
  10. structure OAI.ZeroKey.CausalSampler line 119
  11. def OAI.ZeroKey.CausalSampler.finiteHistory line 129
  12. lemma OAI.ZeroKey.CausalSampler.measurable_finiteHistory line 134
  13. def OAI.ZeroKey.CausalSampler.history line 147
  14. lemma OAI.ZeroKey.CausalSampler.measurable_prefix line 150
  15. lemma OAI.ZeroKey.CausalSampler.prefix_succ line 153
  16. lemma OAI.ZeroKey.CausalSampler.prefix_fresh_independent line 156
  17. lemma OAI.ZeroKey.CausalSampler.prefix_fresh_law line 160
  18. theorem OAI.ZeroKey.CausalSampler.prefix_law_succ line 167
  19. def OAI.ZeroKey.CausalSampler.record line 200
  20. lemma OAI.ZeroKey.CausalSampler.measurable_record line 202
  21. lemma OAI.ZeroKey.CausalSampler.prefix_eq_record line 206
  22. theorem OAI.ZeroKey.CausalSampler.finite_law_unique line 216
  23. theorem OAI.ZeroKey.CausalSampler.record_law_unique line 236
  24. theorem OAI.ZeroKey.exists_causal_sampler line 268
  25. lemma OAI.ZeroKey.condIndep_public_prefixes line 291
  26. theorem OAI.ZeroKey.independent_tapes_given_full_transcript line 313
  27. def OAI.ZeroKey.LocalTapeProgram.message line 338
  28. lemma OAI.ZeroKey.LocalTapeProgram.prefix_succ line 341
  29. lemma OAI.ZeroKey.LocalTapeProgram.measurable_prefix line 344
  30. lemma OAI.ZeroKey.LocalTapeProgram.measurable_message line 358
  31. def OAI.ZeroKey.LocalTapeProgram.field line 365
  32. lemma OAI.ZeroKey.LocalTapeProgram.field_le line 368
  33. lemma OAI.ZeroKey.LocalTapeProgram.field_mono line 370
  34. def OAI.ZeroKey.LocalTapeProgram.filtration line 382
  35. lemma OAI.ZeroKey.LocalTapeProgram.field_zero line 387
  36. lemma OAI.ZeroKey.LocalTapeProgram.field_local line 390
  37. theorem OAI.ZeroKey.LocalTapeProgram.tapes_conditionally_independent line 421
  38. def OAI.ZeroKey.LocalTapeProgram.record line 435
  39. lemma OAI.ZeroKey.LocalTapeProgram.measurable_record line 437
  40. lemma OAI.ZeroKey.LocalTapeProgram.prefix_eq_record line 440
  41. lemma OAI.ZeroKey.LocalTapeProgram.full_record_field line 449
  42. theorem OAI.ZeroKey.LocalTapeProgram.final_records_conditionally_independent line 470
  43. theorem OAI.ZeroKey.selected_tapes_law line 504
  44. lemma OAI.ZeroKey.LocalOutcomeSampler.measurable_privatePrefix line 549
  45. def OAI.ZeroKey.LocalOutcomeSampler.tapeProgram line 573
  46. def OAI.ZeroKey.LocalOutcomeSampler.privateRecord line 588
  47. lemma OAI.ZeroKey.LocalOutcomeSampler.measurable_privateRecord line 596
  48. theorem OAI.ZeroKey.LocalOutcomeSampler.final_records_independent line 613
  49. lemma OAI.ZeroKey.LocalOutcomeSampler.measurable_extractPrivate line 628
  50. lemma OAI.ZeroKey.LocalOutcomeSampler.extractPrivate_snoc line 637
  51. lemma OAI.ZeroKey.LocalOutcomeSampler.measurable_publicFrom line 645
  52. lemma OAI.ZeroKey.LocalOutcomeSampler.publicFrom_snoc line 662
  53. lemma OAI.ZeroKey.LocalOutcomeSampler.privatePrefix_snoc line 669
  54. def OAI.ZeroKey.LocalOutcomeSampler.causal line 676
  55. def OAI.ZeroKey.LocalOutcomeSampler.selectedTape line 687
  56. lemma OAI.ZeroKey.LocalOutcomeSampler.measurable_selectedTape line 690
  57. theorem OAI.ZeroKey.LocalOutcomeSampler.replay_matches line 696
  58. def OAI.ZeroKey.LocalOutcomeSampler.outcomeRecord line 733
  59. lemma OAI.ZeroKey.LocalOutcomeSampler.measurable_outcomeRecord line 736
  60. lemma OAI.ZeroKey.LocalOutcomeSampler.outcomeRecord_law line 739
  61. def OAI.ZeroKey.LocalOutcomeSampler.publicRecord line 753
  62. def OAI.ZeroKey.LocalOutcomeSampler.localRecord line 756
  63. lemma OAI.ZeroKey.LocalOutcomeSampler.measurable_publicRecord line 759
  64. lemma OAI.ZeroKey.LocalOutcomeSampler.measurable_localRecord line 764
  65. lemma OAI.ZeroKey.LocalOutcomeSampler.publicRecord_replay line 772
  66. lemma OAI.ZeroKey.LocalOutcomeSampler.localRecord_replay line 784
  67. theorem OAI.ZeroKey.LocalOutcomeSampler.full_readout_law line 799