OAI/InformationTheory/Entanglement/TensorPowers.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.multiTensor_psd line 14
  2. def OAI.SecretKey.powerMap line 25
  3. lemma OAI.SecretKey.powerMap_single line 39
  4. lemma OAI.SecretKey.powerMap_cp line 43
  5. lemma OAI.SecretKey.powerMap_input_transpose line 53
  6. lemma OAI.SecretKey.powerMap_input_cp line 61
  7. def OAI.SecretKey.pull line 66
  8. lemma OAI.SecretKey.pull_cp line 71
  9. lemma OAI.SecretKey.pull_transpose line 75
  10. lemma OAI.SecretKey.tensorMap_pull line 77
  11. lemma OAI.SecretKey.represented_of_witness line 81
  12. lemma OAI.SecretKey.tensorMap_entry_sum line 110
  13. def OAI.SecretKey.tensorPower line 123
  14. def OAI.SecretKey.vectorPower line 125
  15. lemma OAI.SecretKey.tensorPower_psd line 127
  16. lemma OAI.SecretKey.tensorPower_trace line 131
  17. lemma OAI.SecretKey.powerMap_representation line 141
  18. theorem OAI.SecretKey.represented_tensorPower line 160