OAI/Analysis/HyperbolicCones/FormBasic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Exact identities for the Choi–Lam form.

  1. theorem OAI.Paper256.choiLam_expand line 16
  2. theorem OAI.Paper256.qMatrix_isHermitian line 25
  3. theorem OAI.Paper256.zMatrix_isHermitian line 33
  4. theorem OAI.Paper256.qMatrix_quadratic line 41
  5. theorem OAI.Paper256.zMatrix_quadratic line 46
  6. theorem OAI.Paper256.zMatrix_diag_nonnegative line 51
  7. theorem OAI.Paper256.zMatrix_principal_minor_two line 56
  8. theorem OAI.Paper256.zMatrix_principal_minor_two_nonnegative line 64
  9. theorem OAI.Paper256.zMatrix_det line 71
  10. theorem OAI.Paper256.choiLam_nonzero line 78
  11. theorem OAI.Paper256.choiLam_cyclic_zero line 82
  12. theorem OAI.Paper256.choiLam_sign_zero line 86
  13. theorem OAI.Paper256.choiLam_curve line 91
  14. theorem OAI.Paper256.choiLam_smul_left line 96
  15. theorem OAI.Paper256.choiLam_smul_right line 101