OAI/InformationTheory/SecretKey/Extensions.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UnrestrictedQuantum.deterministicInstrument line 19
  2. def OAI.UnrestrictedQuantum.deterministicRun line 31
  3. lemma OAI.UnrestrictedQuantum.deterministic_event line 46
  4. def OAI.UnrestrictedQuantum.scalarReference line 56
  5. lemma OAI.UnrestrictedQuantum.scalarReference_positive line 62
  6. lemma OAI.UnrestrictedQuantum.scalarReference_one line 68
  7. def OAI.UnrestrictedQuantum.scalarIncoming line 70
  8. def OAI.UnrestrictedQuantum.IncomingObservableProcess.classicalReadout line 87
  9. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.classicalReadout_value line 96
  10. structure OAI.ZeroKey.ConsistentReferenceHistory line 117
  11. def OAI.ZeroKey.ConsistentReferenceHistory.finiteValue line 130
  12. def OAI.ZeroKey.ConsistentReferenceHistory.density line 133
  13. lemma OAI.ZeroKey.ConsistentReferenceHistory.measurable_density line 137
  14. lemma OAI.ZeroKey.ConsistentReferenceHistory.measurable_entry line 140
  15. lemma OAI.ZeroKey.ConsistentReferenceHistory.integrable_entry line 145
  16. lemma OAI.ZeroKey.ConsistentReferenceHistory.integral_entry line 149
  17. lemma OAI.ZeroKey.ConsistentReferenceHistory.density_pos line 158
  18. lemma OAI.ZeroKey.ConsistentReferenceHistory.density_trace line 166
  19. lemma OAI.ZeroKey.ConsistentReferenceHistory.density_entry_martingale_re line 187
  20. lemma OAI.ZeroKey.ConsistentReferenceHistory.density_entry_martingale_im line 205
  21. theorem OAI.ZeroKey.ConsistentReferenceHistory.full_reference_measure line 223
  22. def OAI.ZeroKey.PositiveMatrixMeasure.restrictEvent line 252
  23. lemma OAI.ZeroKey.PositiveMatrixMeasure.restrictEvent_value line 259
  24. lemma OAI.ZeroKey.PositiveMatrixMeasure.eq_of_value line 266
  25. lemma OAI.ZeroKey.PositiveMatrixMeasure.restrictEvent_filter line 280
  26. def OAI.ZeroKey.PositiveMatrixMeasure.testMeasure line 289
  27. instance OAI.ZeroKey.PositiveMatrixMeasure.testMeasure_finite line 292
  28. lemma OAI.ZeroKey.PositiveMatrixMeasure.testMeasure_real line 295
  29. def OAI.ZeroKey.PositiveMatrixMeasure.bitReadout line 303
  30. lemma OAI.ZeroKey.PositiveMatrixMeasure.bitReadout_value line 309
  31. lemma OAI.ZeroKey.PositiveMatrixMeasure.bitReadout_filter line 319
  32. lemma OAI.ZeroKey.scalar_measure_ext_on_filtration line 334
  33. theorem OAI.ZeroKey.ConsistentReferenceHistory.full_reference_born line 364
  34. lemma OAI.ZeroKey.PositiveMatrixMeasure.value_sum_readout line 392
  35. lemma OAI.ZeroKey.PositiveMatrixMeasure.bitReadout_total line 415
  36. theorem OAI.ZeroKey.PositiveMatrixMeasure.filtered_bitReadout_normalized line 426
  37. structure OAI.ZeroKey.ClassicalProtocol line 467
  38. structure OAI.ZeroKey.ClassicalProtocol.Completion line 485
  39. lemma OAI.ZeroKey.ClassicalProtocol.completion_exists line 506
  40. def OAI.ZeroKey.ClassicalProtocol.completion line 512
  41. def OAI.ZeroKey.ClassicalProtocol.toFinite line 514
  42. lemma OAI.ZeroKey.ClassicalProtocol.completeReference_value line 526
  43. theorem OAI.ZeroKey.ClassicalProtocol.output_event line 534
  44. theorem OAI.ZeroKey.ClassicalProtocol.canonicalOutput_event line 551
  45. lemma OAI.ZeroKey.PositiveMatrixMeasure.value_eq_of_ae_set line 574
  46. theorem OAI.ZeroKey.PositiveMatrixMeasure.bitReadout_eq_off_private_null line 582
  47. theorem OAI.ZeroKey.PositiveMatrixMeasure.prepared_default_outputs line 609
  48. theorem OAI.UnrestrictedQuantum.tensor_filter_precompose line 652
  49. theorem OAI.UnrestrictedQuantum.tensor_filter_event line 662
  50. theorem OAI.UnrestrictedQuantum.InstrumentRun.tensor_event line 684
  51. theorem OAI.UnrestrictedQuantum.InstrumentRun.filtered_tensor_event line 696
  52. theorem OAI.ZeroKey.BitProtocol.filtered_output_event line 727
  53. def OAI.ZeroKey.ClassicalProtocol.toBit line 763
  54. lemma OAI.ZeroKey.ClassicalProtocol.toBit_completeReference line 765
  55. lemma OAI.ZeroKey.ClassicalProtocol.toBit_probeOutput line 768
  56. theorem OAI.ZeroKey.ClassicalProtocol.toBit_purifiedOutput line 776
  57. theorem OAI.ZeroKey.ClassicalProtocol.prepared_actual_output line 791
  58. def OAI.UnrestrictedQuantum.independentCoinInstrument line 832
  59. def OAI.UnrestrictedQuantum.independentCoinRun line 837
  60. lemma OAI.UnrestrictedQuantum.independentCoinRun_reference line 852