OAI/InformationTheory/AmplitudeDamping/GramMatrices.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GAD.zeroBlock line 24
  2. def OAI.GAD.gram line 27
  3. def OAI.GAD.mass line 29
  4. def OAI.GAD.logGram line 31
  5. theorem OAI.GAD.mass_nonneg line 34
  6. theorem OAI.GAD.one_add_gram_posDef line 38
  7. theorem OAI.GAD.gram_zeroBlock line 42
  8. theorem OAI.GAD.mass_zeroBlock line 47
  9. theorem OAI.GAD.resolvent_complement line 51
  10. theorem OAI.GAD.det_one_add_gram_zeroBlock line 65
  11. theorem OAI.GAD.logGram_zeroBlock line 83
  12. theorem OAI.GAD.gram_sqrt_smul line 97
  13. theorem OAI.GAD.logDetShift_eq_logGram line 103
  14. theorem OAI.GAD.logDetShift_zeroBlock line 108
  15. theorem OAI.GAD.log_norm_det_diagonal_real line 127
  16. theorem OAI.GAD.blockLogDet_diagonal_real line 133
  17. theorem OAI.GAD.logDetShift_diagonal_real line 165