OAI/InformationTheory/AmplitudeDamping/BlockFactors.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GAD.blockUnitary line 17
  2. theorem OAI.GAD.entropy_blockDiagonal line 29
  3. def OAI.GAD.blockProjection line 54
  4. def OAI.GAD.blockInjection line 57
  5. theorem OAI.GAD.blockProjection_isProjection line 60
  6. theorem OAI.GAD.blockProjection_mul line 68
  7. theorem OAI.GAD.blockInjection_mul line 73
  8. theorem OAI.GAD.blockInjection_isometry line 77
  9. theorem OAI.GAD.blockProjection_range line 84
  10. theorem OAI.GAD.mass_isometry line 94
  11. theorem OAI.GAD.entropy_gram_isometry line 102
  12. theorem OAI.GAD.block_factor_entropy line 110
  13. theorem OAI.GAD.gram_blockInjection line 115
  14. theorem OAI.GAD.trace_product_nonneg line 132
  15. theorem OAI.GAD.trace_product_mono line 141
  16. theorem OAI.GAD.IsState.le_one line 146
  17. theorem OAI.GAD.state_measurement_prob_le_trace line 173