OAI/InformationTheory/Entanglement/TraceMatrixSpace.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.traceNorm_eq_zero line 11
  2. lemma OAI.SecretKey.traceNorm_real_smul line 24
  3. structure OAI.SecretKey.TraceMatrix line 36
  4. def OAI.SecretKey.TraceMatrix.toEquiv line 39
  5. instance OAI.SecretKey.TraceMatrix.traceMatrixAddCommGroup line 44
  6. instance OAI.SecretKey.TraceMatrix.traceMatrixModule line 45
  7. def OAI.SecretKey.TraceMatrix.equiv line 46
  8. instance OAI.SecretKey.TraceMatrix.traceMatrixNormedAddCommGroup line 47
  9. lemma OAI.SecretKey.TraceMatrix.norm_eq line 53
  10. instance OAI.SecretKey.TraceMatrix.traceMatrixNormedSpace line 54
  11. instance OAI.SecretKey.TraceMatrix.traceMatrixFiniteDimensional line 58
  12. instance OAI.SecretKey.TraceMatrix.traceMatrixCompleteSpace line 59
  13. def OAI.SecretKey.TraceMatrix.equivL line 60
  14. instance OAI.SecretKey.TraceMatrix.traceMatrixMeasurableSpace line 61
  15. instance OAI.SecretKey.TraceMatrix.traceMatrixBorelSpace line 62
  16. instance OAI.SecretKey.TraceMatrix.traceMatrixSecondCountableTopology line 63
  17. lemma OAI.SecretKey.TraceMatrix.measurable_into line 66
  18. lemma OAI.SecretKey.TraceMatrix.integrable_into line 69
  19. lemma OAI.SecretKey.TraceMatrix.setIntegral_entry line 86