OAI/Analysis/MatrixSigning/Optimization/AffineRealEval.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentKS.RationalSDP.Pencil.ofAffine_realEval line 14
  2. lemma OAI.CurrentKS.RationalSDP.realFinDecode_cast line 30
  3. lemma OAI.CurrentKS.RationalSDP.matrixVariable_cast line 35
  4. lemma OAI.CurrentKS.RationalSDP.cast_matrix_sum line 42
  5. lemma OAI.CurrentKS.RationalSDP.cast_matrix_smul line 46
  6. lemma OAI.CurrentKS.RationalSDP.cast_matrix_one line 50
  7. lemma OAI.CurrentKS.RationalSDP.cast_matrix_zero line 52
  8. lemma OAI.CurrentKS.RationalSDP.cast_matrix_add line 55
  9. lemma OAI.CurrentKS.RationalSDP.cast_matrix_sub line 59
  10. lemma OAI.CurrentKS.RationalSDP.cast_matrix_neg line 63
  11. lemma OAI.CurrentKS.RationalSDP.cast_matrix_mul line 67
  12. lemma OAI.CurrentKS.RationalSDP.rationalSum_cast line 71
  13. lemma OAI.CurrentKS.RationalSDP.rationalEta_cast line 76
  14. lemma OAI.CurrentKS.RationalSDP.schurPencil_realEval line 84