OAI/Computability/MeanPayoff/Volume.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.orientationTail_length line 9
  2. theorem OAI.MeanPayoff.orient_length line 31
  3. theorem OAI.MeanPayoff.flatten_length_bound line 57
  4. def OAI.MeanPayoff.globalListBound line 67
  5. theorem OAI.MeanPayoff.orientPlus_length line 69
  6. theorem OAI.MeanPayoff.LowerComparisons.ask_high line 93
  7. theorem OAI.MeanPayoff.LowerComparisons.ask_low line 102
  8. def OAI.MeanPayoff.TightHigh line 111
  9. def OAI.MeanPayoff.TightLow line 116
  10. def OAI.MeanPayoff.TightHighRequest line 121
  11. def OAI.MeanPayoff.TightLowRequest line 126
  12. theorem OAI.MeanPayoff.tightRequest_high line 131
  13. theorem OAI.MeanPayoff.tightRequest_low line 149
  14. theorem OAI.MeanPayoff.floor_update_volume line 167
  15. theorem OAI.MeanPayoff.ceiling_update_volume line 178
  16. theorem OAI.MeanPayoff.volume_error_step line 189
  17. theorem OAI.MeanPayoff.tighten_high line 195
  18. theorem OAI.MeanPayoff.tighten_low line 257