OAI/InformationTheory/AmplitudeDamping/PhaseProducts.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GAD.tensorMatrix line 12
  2. def OAI.GAD.tensorSplit line 15
  3. theorem OAI.GAD.tensorMatrix_split line 18
  4. theorem OAI.GAD.tensorMatrix_trace line 25
  5. theorem OAI.GAD.tensorMatrix_zero line 29
  6. theorem OAI.GAD.tensorMatrix_posSemidef line 34
  7. theorem OAI.GAD.tensorMatrix_state line 45
  8. theorem OAI.GAD.tensorMatrix_entropy line 51
  9. theorem OAI.GAD.channel_tensorMatrix line 66
  10. theorem OAI.GAD.tensorMatrix_sum line 96
  11. theorem OAI.GAD.tensorMatrix_smul line 103
  12. theorem OAI.GAD.tensorMatrix_average line 108
  13. theorem OAI.GAD.phaseState_tensor line 127
  14. theorem OAI.GAD.phaseState_state line 132
  15. theorem OAI.GAD.phaseState_output line 137
  16. theorem OAI.GAD.phaseState_entropy line 142
  17. theorem OAI.GAD.phaseState_average_entropy line 149
  18. theorem OAI.GAD.basis_card line 164
  19. theorem OAI.GAD.phase_weights_sum line 167
  20. theorem OAI.GAD.phaseValue_formula line 171
  21. def OAI.GAD.phaseEnsemble line 180
  22. theorem OAI.GAD.phaseEnsemble_value line 190