OAI/InformationTheory/AmplitudeDamping/StateEntropy.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.GAD.state_mixture line 15
  2. theorem OAI.GAD.spectral_pure_decomposition line 24
  3. theorem OAI.GAD.spectral_weights_sum line 38
  4. theorem OAI.GAD.spectral_vectors_mass line 43
  5. theorem OAI.GAD.channel_mixture line 47
  6. def OAI.GAD.matrixPopulation line 53
  7. theorem OAI.GAD.matrixPopulation_pure line 56
  8. theorem OAI.GAD.matrixPopulation_mixture line 60
  9. theorem OAI.GAD.matrixPopulation_nonneg line 70
  10. theorem OAI.GAD.matrixPopulation_le_trace line 78
  11. theorem OAI.GAD.matrixPopulation_mem line 87
  12. def OAI.GAD.spectralFactor line 101
  13. theorem OAI.GAD.spectralFactor_gram line 104
  14. theorem OAI.GAD.spectralFactor_column line 121
  15. theorem OAI.GAD.entropy_sum_le line 126
  16. theorem OAI.GAD.entropy_mixture_upper line 147