OAI/Analysis/MatrixSigning/Realization/OptimizeRealization.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CurrentKS.Realization.OptParams line 14
  2. abbrev OAI.CurrentKS.Realization.optScalarsCode line 23
  3. abbrev OAI.CurrentKS.Realization.optDataCode line 24
  4. def OAI.CurrentKS.Realization.optData line 25
  5. def OAI.CurrentKS.Realization.optCode line 26
  6. def OAI.CurrentKS.Realization.optView line 27
  7. def OAI.CurrentKS.Realization.optB line 29
  8. def OAI.CurrentKS.Realization.optF line 31
  9. def OAI.CurrentKS.Realization.optScalars line 34
  10. def OAI.CurrentKS.Realization.optDelta line 37
  11. def OAI.CurrentKS.Realization.optRest line 39
  12. def OAI.CurrentKS.Realization.optRadius line 41
  13. def OAI.CurrentKS.Realization.optUpper line 44
  14. def OAI.CurrentKS.Realization.optLevel line 47
  15. def OAI.CurrentKS.Realization.optLevelPencil line 52
  16. def OAI.CurrentKS.Realization.candidateSearch line 58
  17. def OAI.CurrentKS.Realization.optCandidate line 60
  18. structure OAI.CurrentKS.Realization.OptState line 72
  19. def OAI.CurrentKS.Realization.optStateData line 77
  20. abbrev OAI.CurrentKS.Realization.optStateDataCode line 78
  21. def OAI.CurrentKS.Realization.optStateCode line 79
  22. def OAI.CurrentKS.Realization.optStateView line 80
  23. def OAI.CurrentKS.Realization.osP line 82
  24. def OAI.CurrentKS.Realization.osK line 84
  25. def OAI.CurrentKS.Realization.osY line 86
  26. def OAI.CurrentKS.Realization.OptState.feasibility line 88
  27. def OAI.CurrentKS.Realization.osFeasible line 90
  28. def OAI.CurrentKS.Realization.OptState.next line 95
  29. def OAI.CurrentKS.Realization.osNext line 98
  30. def OAI.CurrentKS.Realization.OptParams.init line 105
  31. def OAI.CurrentKS.Realization.optInit line 107
  32. lemma OAI.CurrentKS.Realization.opt_iterate line 112
  33. def OAI.CurrentKS.Realization.optimize line 118