OAI/InformationTheory/Entanglement/MatrixTraceMeasure.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecretKey.PositiveMatrixMeasure.traceSigned line 14
  2. lemma OAI.SecretKey.PositiveMatrixMeasure.traceSigned_apply line 15
  3. lemma OAI.SecretKey.PositiveMatrixMeasure.traceSigned_nonneg line 18
  4. def OAI.SecretKey.PositiveMatrixMeasure.traceMeasure line 26
  5. instance OAI.SecretKey.PositiveMatrixMeasure.(instance at line 28) line 28
  6. lemma OAI.SecretKey.PositiveMatrixMeasure.traceMeasure_real line 29
  7. lemma OAI.SecretKey.PositiveMatrixMeasure.trace_domination line 33
  8. def OAI.SecretKey.PositiveMatrixMeasure.positiveDensity line 38
  9. lemma OAI.SecretKey.PositiveMatrixMeasure.positiveDensity_psd line 40
  10. lemma OAI.SecretKey.PositiveMatrixMeasure.positiveDensity_measurable line 45
  11. lemma OAI.SecretKey.PositiveMatrixMeasure.positiveDensity_ae_eq line 51
  12. lemma OAI.SecretKey.PositiveMatrixMeasure.positiveDensity_integrable line 55
  13. lemma OAI.SecretKey.PositiveMatrixMeasure.positiveDensity_setIntegral line 60
  14. lemma OAI.SecretKey.PositiveMatrixMeasure.positiveDensity_trace_integrable line 66
  15. lemma OAI.SecretKey.PositiveMatrixMeasure.positiveDensity_trace_setIntegral line 69