OAI/InformationTheory/SecretKey/Discussion.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroKey.globalLocalReferenceA line 30
  2. def OAI.ZeroKey.globalLocalReferenceB line 33
  3. lemma OAI.ZeroKey.globalLocalReferenceA_measurable line 37
  4. lemma OAI.ZeroKey.globalLocalReferenceB_measurable line 43
  5. lemma OAI.ZeroKey.globalLocalReferenceA_mean line 49
  6. lemma OAI.ZeroKey.globalLocalReferenceB_mean line 69
  7. def OAI.ZeroKey.jointReference line 88
  8. lemma OAI.ZeroKey.jointReference_density line 92
  9. lemma OAI.ZeroKey.jointReference_measurable line 98
  10. lemma OAI.ZeroKey.jointReference_mean line 112
  11. theorem OAI.ZeroKey.exists_adaptive_instrument_sampler line 152
  12. lemma OAI.ZeroKey.publicMatrix_positive line 185
  13. lemma OAI.ZeroKey.PositiveMatrixMeasure.filter_eq_of_filtration line 204
  14. lemma OAI.UnrestrictedQuantum.bitReference_total_trace line 233
  15. lemma OAI.UnrestrictedQuantum.bitReference_filter line 240
  16. def OAI.UnrestrictedQuantum.tensorReferenceFunctional line 260
  17. lemma OAI.UnrestrictedQuantum.tensorReferenceFunctional_apply line 266
  18. theorem OAI.UnrestrictedQuantum.tensorReferenceFunctional_precompose line 270
  19. lemma OAI.UnrestrictedQuantum.product_event_reference line 279