OAI/Analysis/MatrixSigning/Optimization/ValueDimension.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.RationalSDP.valueDimension line 15
  2. def OAI.CurrentKS.RationalSDP.valueIndex line 17
  3. def OAI.CurrentKS.RationalSDP.timeCoordinate line 22
  4. def OAI.CurrentKS.RationalSDP.matrixCoordinate line 25
  5. def OAI.CurrentKS.RationalSDP.realFinDecode line 30
  6. lemma OAI.CurrentKS.RationalSDP.realFinDecode_symm line 36
  7. def OAI.CurrentKS.RationalSDP.matrixVariable line 39
  8. lemma OAI.CurrentKS.RationalSDP.matrixVariable_symm line 43
  9. def OAI.CurrentKS.RationalSDP.sandwichLinear line 49
  10. lemma OAI.CurrentKS.RationalSDP.sandwichLinear_symm line 55
  11. def OAI.CurrentKS.RationalSDP.rationalSum line 60
  12. lemma OAI.CurrentKS.RationalSDP.rationalSum_symm line 63
  13. def OAI.CurrentKS.RationalSDP.rationalEta line 71
  14. lemma OAI.CurrentKS.RationalSDP.rationalEta_symm line 75
  15. def OAI.CurrentKS.RationalSDP.identityLinear line 85
  16. def OAI.CurrentKS.RationalSDP.diagonalLinear line 91
  17. def OAI.CurrentKS.RationalSDP.schurPencil line 104
  18. def OAI.CurrentKS.RationalSDP.lowerMatrixPencil line 125
  19. def OAI.CurrentKS.RationalSDP.upperMatrixPencil line 129
  20. def OAI.CurrentKS.RationalSDP.lowerTimePencil line 133
  21. def OAI.CurrentKS.RationalSDP.upperTimePencil line 136
  22. def OAI.CurrentKS.RationalSDP.valuePencil line 141
  23. def OAI.CurrentKS.RationalSDP.valueObjective line 147
  24. lemma OAI.CurrentKS.RationalSDP.schurPencil_eval line 151
  25. lemma OAI.CurrentKS.RationalSDP.lowerMatrixPencil_eval line 165
  26. lemma OAI.CurrentKS.RationalSDP.upperMatrixPencil_eval line 170
  27. lemma OAI.CurrentKS.RationalSDP.valueObjective_apply line 174