OAI/InformationTheory/Entanglement/FactorizedLawGap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecretKey.bitComparisonMeasure line 13
  2. instance OAI.SecretKey.bitComparisonMeasureIsFiniteMeasure line 16
  3. lemma OAI.SecretKey.bitComparison_actual_dom line 21
  4. lemma OAI.SecretKey.bitComparison_ideal_dom line 27
  5. def OAI.SecretKey.cqBitDistance line 31
  6. lemma OAI.SecretKey.cqBitDistance_enlarge line 35
  7. lemma OAI.SecretKey.integral_trace_of_entry_integrals line 42
  8. lemma OAI.SecretKey.measurable_factorized_eveBlock line 51
  9. lemma OAI.SecretKey.scaled_eveBlock_coherence line 71
  10. theorem OAI.SecretKey.factorized_law_gap line 87