OAI/InformationTheory/Entanglement/DensityGap.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SecretKey.matrixMeasurableSpace line 11
  2. instance OAI.SecretKey.matrixBorelSpace line 12
  3. lemma OAI.SecretKey.traceNorm_neg line 15
  4. lemma OAI.SecretKey.traceNorm_sub_le line 18
  5. lemma OAI.SecretKey.traceNorm_sub_triangle line 20
  6. lemma OAI.SecretKey.trace_sub_reverse_le line 25
  7. lemma OAI.SecretKey.integrable_traceNorm_sub line 32
  8. def OAI.SecretKey.halfDensity line 44
  9. lemma OAI.SecretKey.halfDensity_psd line 46
  10. lemma OAI.SecretKey.halfDensity_trace line 49
  11. def OAI.SecretKey.idealDensity line 54
  12. def OAI.SecretKey.bitDistance line 56
  13. theorem OAI.SecretKey.matrix_density_gap line 59