OAI/Computability/MeanPayoff/RootBox.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.auxiliaryCalls line 9
  2. def OAI.MeanPayoff.chainBound line 14
  3. def OAI.MeanPayoff.callBase line 16
  4. def OAI.MeanPayoff.callBound line 18
  5. theorem OAI.MeanPayoff.CountedAlgorithm.bounded_solveWidth line 22
  6. theorem OAI.MeanPayoff.CountedAlgorithm.bounded_solveWidth_global line 82
  7. theorem OAI.MeanPayoff.CountedAlgorithm.bounded_solve line 94
  8. theorem OAI.MeanPayoff.parameterRank_nat_bound line 129
  9. theorem OAI.MeanPayoff.rootRank_bound line 146
  10. def OAI.MeanPayoff.SolveBox.SafeEndpoints line 163
  11. theorem OAI.MeanPayoff.SolveBox.safe_of_inside line 167
  12. theorem OAI.MeanPayoff.SolveBox.safe_centered line 177
  13. theorem OAI.MeanPayoff.SolveBox.safe_withFloor line 190
  14. theorem OAI.MeanPayoff.SolveBox.safe_withCeiling line 194
  15. theorem OAI.MeanPayoff.SolveBox.safe_capLow line 198
  16. theorem OAI.MeanPayoff.SolveBox.safe_capHigh line 203
  17. theorem OAI.MeanPayoff.SolveBox.eight_D_le line 208
  18. theorem OAI.MeanPayoff.SolveBox.safe_narrowCentered line 214
  19. theorem OAI.MeanPayoff.SolveBox.safe_wideCentered line 219
  20. theorem OAI.MeanPayoff.SolveBox.safe_vector_bound line 225
  21. theorem OAI.MeanPayoff.SolveBox.safe_vector_abs line 233
  22. theorem OAI.MeanPayoff.rootBox_safe line 242
  23. inductive OAI.MeanPayoff.ReachableBox line 248
  24. theorem OAI.MeanPayoff.ReachableBox.safe line 256