OAI/Computability/MeanPayoff/Tightening.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.globalJ_quadratic line 9
  2. theorem OAI.MeanPayoff.geometric_error line 18
  3. theorem OAI.MeanPayoff.orientation_error_small line 30
  4. theorem OAI.MeanPayoff.orient_high_small line 54
  5. theorem OAI.MeanPayoff.orient_low_small line 68
  6. theorem OAI.MeanPayoff.RandomTree.filter_le_badCount line 85
  7. theorem OAI.MeanPayoff.bool_filter_partition line 100
  8. theorem OAI.MeanPayoff.exception_retained line 108
  9. theorem OAI.MeanPayoff.combine_high_failure line 113
  10. theorem OAI.MeanPayoff.combine_low_failure line 130
  11. theorem OAI.MeanPayoff.orientPlus_high line 146
  12. theorem OAI.MeanPayoff.orientPlus_low line 162
  13. theorem OAI.MeanPayoff.AdmissibleSub.raise_floor line 183
  14. theorem OAI.MeanPayoff.AdmissibleSuper.lower_ceiling line 192
  15. theorem OAI.MeanPayoff.AdmissibleSub.restrict_ceiling line 201
  16. theorem OAI.MeanPayoff.AdmissibleSuper.restrict_floor line 206
  17. def OAI.MeanPayoff.tightSub line 211
  18. def OAI.MeanPayoff.tightSuper line 213
  19. theorem OAI.MeanPayoff.SolveBox.delta_bounds line 216
  20. theorem OAI.MeanPayoff.tightSub_solution line 226
  21. theorem OAI.MeanPayoff.tightSuper_solution line 252
  22. theorem OAI.MeanPayoff.tightSub_core line 278
  23. theorem OAI.MeanPayoff.tightSuper_core line 294
  24. theorem OAI.MeanPayoff.tightSub_forces_update line 310
  25. theorem OAI.MeanPayoff.tightSuper_forces_update line 317