OAI/Analysis/MatrixSigning/Complexity/PSDControllerPolynomial.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W23.PSDControllerPolynomial.X line 12
  2. def OAI.KS.W23.PSDControllerPolynomial.inverseP line 13
  3. def OAI.KS.W23.PSDControllerPolynomial.matrixP line 15
  4. def OAI.KS.W23.PSDControllerPolynomial.witnessHeightP line 16
  5. def OAI.KS.W23.PSDControllerPolynomial.witnessP line 17
  6. def OAI.KS.W23.PSDControllerPolynomial.frameP line 18
  7. def OAI.KS.W23.PSDControllerPolynomial.replayInputP line 19
  8. def OAI.KS.W23.PSDControllerPolynomial.replayP line 20
  9. def OAI.KS.W23.PSDControllerPolynomial.terminalP line 22
  10. def OAI.KS.W23.PSDControllerPolynomial.stepP line 25
  11. def OAI.KS.W23.PSDControllerPolynomial.controllerPolynomial line 28
  12. def OAI.KS.W23.PSDControllerPolynomial.coefficient line 31
  13. theorem OAI.KS.W23.PSDControllerPolynomial.expression_eval line 33
  14. theorem OAI.KS.W23.PSDControllerPolynomial.expression_degree line 35
  15. theorem OAI.KS.W23.PSDControllerPolynomial.originalControllerBound_mono_dim line 37
  16. theorem OAI.KS.W23.PSDControllerPolynomial.originalControllerBound_le_monomial line 45
  17. theorem OAI.KS.W23.PSDControllerPolynomial.controller_polynomial_spec line 54