OAI/Analysis/MatrixSigning/Complexity/PolynomialOptimize.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CurrentKS.Realization.poly_optView line 14
  2. instance OAI.CurrentKS.Realization.poly_optB line 15
  3. instance OAI.CurrentKS.Realization.poly_optF line 16
  4. instance OAI.CurrentKS.Realization.poly_optScalars line 17
  5. instance OAI.CurrentKS.Realization.poly_optDelta line 18
  6. instance OAI.CurrentKS.Realization.poly_optRest line 19
  7. instance OAI.CurrentKS.Realization.poly_optRadius line 20
  8. instance OAI.CurrentKS.Realization.poly_optUpper line 21
  9. instance OAI.CurrentKS.Realization.poly_optLevel line 22
  10. instance OAI.CurrentKS.Realization.poly_optLevelPencil line 23
  11. instance OAI.CurrentKS.Realization.poly_optStateView line 24
  12. instance OAI.CurrentKS.Realization.poly_osP line 25
  13. instance OAI.CurrentKS.Realization.poly_osK line 26
  14. instance OAI.CurrentKS.Realization.poly_osY line 27
  15. instance OAI.CurrentKS.Realization.poly_isPSD line 28
  16. instance OAI.CurrentKS.Realization.poly_witnessStateView line 29
  17. instance OAI.CurrentKS.Realization.poly_witnessEvaluation line 30
  18. instance OAI.CurrentKS.Realization.poly_witnessNone line 31
  19. instance OAI.CurrentKS.Realization.poly_osFeasible line 32
  20. lemma OAI.CurrentKS.Realization.RunsPoly.then_with line 38
  21. def OAI.CurrentKS.Realization.OptParams.searchCount line 45
  22. lemma OAI.CurrentKS.Realization.runsPoly_optCandidate line 47
  23. def OAI.CurrentKS.Realization.candidateResource line 57
  24. lemma OAI.CurrentKS.Realization.candidate_cost_bound line 58
  25. lemma OAI.CurrentKS.Realization.candidate_length_bound line 66
  26. lemma OAI.CurrentKS.Realization.runsPoly_osNext line 77
  27. def OAI.CurrentKS.Realization.nextResource line 91
  28. lemma OAI.CurrentKS.Realization.osNext_cost_bound line 92
  29. lemma OAI.CurrentKS.Realization.optimize_is_candidate line 96
  30. lemma OAI.CurrentKS.Realization.runsPoly_optInit line 108
  31. lemma OAI.CurrentKS.Realization.opt_iterate_size_bound line 121
  32. lemma OAI.CurrentKS.Realization.optimize_loop_cost_bound line 135
  33. lemma OAI.CurrentKS.Realization.runsPoly_optimize line 157