OAI/InformationTheory/Entanglement/CQVariation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecretKey.traceDensityMeasure line 13
  2. lemma OAI.SecretKey.traceDensityMeasure_value line 15
  3. lemma OAI.SecretKey.traceDensityMeasure_variation line 21
  4. lemma OAI.SecretKey.idealDensity_entry_integrable line 32
  5. lemma OAI.SecretKey.idealDensity_entry_integral line 40
  6. def OAI.SecretKey.cqDifferenceMeasure line 46
  7. lemma OAI.SecretKey.cqDifferenceMeasure_value line 51
  8. theorem OAI.SecretKey.cqBitDistance_variation line 69