OAI/Computability/MeanPayoff/Drift.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.epsilon line 9
  2. theorem OAI.MeanPayoff.epsilon_nonneg line 11
  3. def OAI.MeanPayoff.HighStep line 14
  4. def OAI.MeanPayoff.LowStep line 20
  5. theorem OAI.MeanPayoff.centerUpdate_movement line 26
  6. theorem OAI.MeanPayoff.centerUpdate_high line 40
  7. theorem OAI.MeanPayoff.centerUpdate_low_deterministic line 84
  8. theorem OAI.MeanPayoff.RandomTree.pair_error line 102
  9. theorem OAI.MeanPayoff.average_low_error line 113
  10. theorem OAI.MeanPayoff.centerUpdate_low line 131
  11. def OAI.MeanPayoff.Linked line 164
  12. theorem OAI.MeanPayoff.linked_single line 167
  13. theorem OAI.MeanPayoff.linked_cons line 170
  14. def OAI.MeanPayoff.CenterDrift line 178
  15. theorem OAI.MeanPayoff.centerDrift_start line 181
  16. theorem OAI.MeanPayoff.centerDrift_mono line 185
  17. theorem OAI.MeanPayoff.centerDrift_move line 190
  18. theorem OAI.MeanPayoff.centerSteps_length line 200
  19. theorem OAI.MeanPayoff.centerSteps_relation line 213
  20. theorem OAI.MeanPayoff.centerSteps_high line 242
  21. theorem OAI.MeanPayoff.centerSteps_low line 263