OAI/InformationTheory/AmplitudeDamping/Channel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.GAD.kraus_zero line 14
  2. theorem OAI.GAD.kraus_one line 17
  3. theorem OAI.GAD.kraus_two line 20
  4. theorem OAI.GAD.kraus_three line 23
  5. theorem OAI.GAD.sum_fin_cons line 26
  6. def OAI.GAD.pure line 33
  7. def OAI.GAD.applyKraus line 35
  8. theorem OAI.GAD.local_channel line 39
  9. theorem OAI.GAD.kraus_complete line 61
  10. theorem OAI.GAD.tensorKraus_complete line 87
  11. theorem OAI.GAD.applyKraus_posSemidef line 111
  12. theorem OAI.GAD.applyKraus_trace line 118
  13. theorem OAI.GAD.channel_trace line 131
  14. theorem OAI.GAD.channel_posSemidef line 136
  15. theorem OAI.GAD.mul_pure_mul_conjTranspose line 139
  16. def OAI.GAD.columns line 145
  17. theorem OAI.GAD.columns_mul_conjTranspose line 148
  18. theorem OAI.GAD.columns_pure line 156