OAI/InformationTheory/Entanglement/DensityChange.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.traceNorm_smul_nonneg line 11
  2. lemma OAI.SecretKey.eveBlock_smul line 20
  3. def OAI.SecretKey.densityWeight line 24
  4. lemma OAI.SecretKey.densityWeight_nonneg line 25
  5. lemma OAI.SecretKey.densityWeight_measurable line 26
  6. lemma OAI.SecretKey.densityWeight_integrable line 30
  7. lemma OAI.SecretKey.densityWeight_integral line 35
  8. lemma OAI.SecretKey.densityWeight_setIntegral line 40
  9. lemma OAI.SecretKey.densityWeight_eveBlock line 47
  10. lemma OAI.SecretKey.densityWeight_traceNorm_integral line 53