OAI/Computability/MeanPayoff/Recursion.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.Budgets.reduceK_rank line 9
  2. theorem OAI.MeanPayoff.Budgets.reduceM_rank line 15
  3. theorem OAI.MeanPayoff.Budgets.reweightK_rank line 21
  4. theorem OAI.MeanPayoff.Budgets.reweightM_rank line 26
  5. abbrev OAI.MeanPayoff.LowerSolver line 31
  6. abbrev OAI.MeanPayoff.SmallSet line 35
  7. structure OAI.MeanPayoff.Orientation line 37
  8. def OAI.MeanPayoff.SolveBox.D line 43
  9. def OAI.MeanPayoff.SolveBox.E line 44
  10. def OAI.MeanPayoff.SolveBox.delta line 45
  11. def OAI.MeanPayoff.SolveBox.C line 46
  12. theorem OAI.MeanPayoff.SolveBox.D_positive line 48
  13. theorem OAI.MeanPayoff.SolveBox.D_small line 53
  14. theorem OAI.MeanPayoff.SolveBox.E_positive line 59
  15. theorem OAI.MeanPayoff.SolveBox.E_smaller line 64
  16. theorem OAI.MeanPayoff.SolveBox.delta_positive line 70
  17. theorem OAI.MeanPayoff.SolveBox.delta_smaller line 75
  18. theorem OAI.MeanPayoff.SolveBox.C_positive line 82
  19. theorem OAI.MeanPayoff.SolveBox.C_smaller line 87
  20. def OAI.MeanPayoff.SolveBox.narrowCentered line 94
  21. def OAI.MeanPayoff.SolveBox.wideCentered line 98
  22. def OAI.MeanPayoff.centerUpdate line 104
  23. def OAI.MeanPayoff.centerSteps line 112
  24. def OAI.MeanPayoff.PositiveDisplacement line 121
  25. def OAI.MeanPayoff.NegativeDisplacement line 125
  26. def OAI.MeanPayoff.orientBase line 129
  27. def OAI.MeanPayoff.orientationTail line 137
  28. def OAI.MeanPayoff.orient line 151
  29. def OAI.MeanPayoff.combineOrientations line 163
  30. def OAI.MeanPayoff.orientPlus line 167
  31. structure OAI.MeanPayoff.InnerBox line 173
  32. def OAI.MeanPayoff.InnerBox.include line 179
  33. theorem OAI.MeanPayoff.volume_ceiling_decreases line 183
  34. def OAI.MeanPayoff.tighten line 195
  35. def OAI.MeanPayoff.RandomTree.traverse line 227
  36. def OAI.MeanPayoff.SolveBox.maxVector line 235
  37. def OAI.MeanPayoff.SolveBox.minVector line 243
  38. def OAI.MeanPayoff.SolveBox.includeCapLow line 251
  39. def OAI.MeanPayoff.SolveBox.includeCapHigh line 255
  40. def OAI.MeanPayoff.finishChoice line 261
  41. def OAI.MeanPayoff.solveWidth line 278
  42. def OAI.MeanPayoff.solve line 299