OAI/InformationTheory/Entanglement/TraceTensor.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.hilbertTensorMap_nonneg line 13
  2. lemma OAI.SecretKey.tensor_positive_diagonal line 26
  3. lemma OAI.SecretKey.tensor_positive_trace line 33
  4. lemma OAI.SecretKey.hilbertTmul_add_left line 49
  5. lemma OAI.SecretKey.hilbertTmul_add_right line 53
  6. lemma OAI.SecretKey.hilbertTmul_smul_left line 57
  7. lemma OAI.SecretKey.hilbertTmul_smul_right line 61
  8. lemma OAI.SecretKey.hilbertTensorMap_add_left line 65
  9. lemma OAI.SecretKey.hilbertTensorMap_add_right line 71
  10. lemma OAI.SecretKey.hilbertTensorMap_smul_left line 77
  11. lemma OAI.SecretKey.hilbertTensorMap_smul_right line 83
  12. lemma OAI.SecretKey.hilbertTensorMap_zero_left line 89
  13. lemma OAI.SecretKey.hilbertTensorMap_zero_right line 96
  14. lemma OAI.SecretKey.tensor_traceClass_mem line 102
  15. def OAI.SecretKey.traceTensor line 121
  16. lemma OAI.SecretKey.traceTensor_trace line 124