OAI/InformationTheory/AmplitudeDamping/Pinching.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.GAD.inv_unitary_conj line 23
  2. theorem OAI.GAD.blockLogDet_unitary line 32
  3. def OAI.GAD.flipSign line 52
  4. def OAI.GAD.partialPinch line 64
  5. theorem OAI.GAD.partialPinch_empty line 68
  6. theorem OAI.GAD.partialPinch_univ line 71
  7. theorem OAI.GAD.flipSign_conj_apply line 76
  8. theorem OAI.GAD.partialPinch_insert line 82
  9. theorem OAI.GAD.flipSign_diagonal line 96
  10. theorem OAI.GAD.partialPinch_posDef line 105
  11. theorem OAI.GAD.blockLogDet_partialPinch_le line 115
  12. theorem OAI.GAD.blockLogDet_diagonal_le line 141