OAI/Computability/MeanPayoff/GridLabels.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.Label.massLabels line 9
  2. theorem OAI.MeanPayoff.Label.massBase_good line 11
  3. def OAI.MeanPayoff.Label.widthLabels line 28
  4. theorem OAI.MeanPayoff.Label.widthBase_good line 31
  5. abbrev OAI.MeanPayoff.Label.Grid line 48
  6. def OAI.MeanPayoff.Label.gridPivot line 50
  7. def OAI.MeanPayoff.Label.gridCenter line 53
  8. def OAI.MeanPayoff.Label.gridDown line 55
  9. def OAI.MeanPayoff.Label.gridUp line 58
  10. theorem OAI.MeanPayoff.Label.gridPivot_center line 61
  11. theorem OAI.MeanPayoff.Label.gridPivot_bounds line 66
  12. theorem OAI.MeanPayoff.Label.gridPivot_mono line 73
  13. theorem OAI.MeanPayoff.Label.gridDown_le line 80
  14. theorem OAI.MeanPayoff.Label.le_gridUp line 88
  15. theorem OAI.MeanPayoff.Label.gridPivot_down line 97
  16. theorem OAI.MeanPayoff.Label.gridPivot_up line 116
  17. def OAI.MeanPayoff.Label.settle line 135
  18. theorem OAI.MeanPayoff.Label.settle_invariant line 150
  19. def OAI.MeanPayoff.Label.downRank line 160
  20. def OAI.MeanPayoff.Label.upRank line 162
  21. theorem OAI.MeanPayoff.Label.downRank_le line 164
  22. theorem OAI.MeanPayoff.Label.upRank_le line 170
  23. theorem OAI.MeanPayoff.Label.downRank_strict line 175
  24. theorem OAI.MeanPayoff.Label.upRank_strict line 183
  25. def OAI.MeanPayoff.Label.downRun line 193
  26. def OAI.MeanPayoff.Label.upRun line 197
  27. theorem OAI.MeanPayoff.Label.downRun_le line 201
  28. theorem OAI.MeanPayoff.Label.le_upRun line 206
  29. theorem OAI.MeanPayoff.Label.downRun_peak line 211
  30. theorem OAI.MeanPayoff.Label.upRun_peak line 227
  31. def OAI.MeanPayoff.Label.downPivot line 243
  32. def OAI.MeanPayoff.Label.finalGrid line 246
  33. def OAI.MeanPayoff.Label.finalPivot line 249
  34. theorem OAI.MeanPayoff.Label.passes_good line 252