OAI/Analysis/HyperbolicCones/MatrixBasic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Paper256.sym_isHermitian line 14
  2. theorem OAI.Paper256.qMatrix_smul line 16
  3. theorem OAI.Paper256.phi_add line 21
  4. theorem OAI.Paper256.phi_smul line 29
  5. theorem OAI.Paper256.phi_zero line 37
  6. theorem OAI.Paper256.phi_scaling_general line 40
  7. theorem OAI.Paper256.phi_scaling line 49
  8. theorem OAI.Paper256.phi_zero_parameter line 53
  9. theorem OAI.Paper256.phi_neg_parameter line 57
  10. theorem OAI.Paper256.phi_rank_one line 61
  11. theorem OAI.Paper256.matrixValue_inverse line 68