OAI/Computability/MeanPayoff/Alternatives.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.linked_first line 10
  2. theorem OAI.MeanPayoff.linked_step line 15
  3. def OAI.MeanPayoff.badTimes line 21
  4. theorem OAI.MeanPayoff.badTimes_zero line 24
  5. theorem OAI.MeanPayoff.badTimes_succ line 27
  6. theorem OAI.MeanPayoff.linked_telescope line 33
  7. theorem OAI.MeanPayoff.centerSteps_all_relation line 50
  8. def OAI.MeanPayoff.Moving line 64
  9. theorem OAI.MeanPayoff.centerSteps_moving line 67
  10. theorem OAI.MeanPayoff.centerSteps_metadata line 74
  11. theorem OAI.MeanPayoff.linked_drift line 83
  12. def OAI.MeanPayoff.HighBad line 90
  13. def OAI.MeanPayoff.LowBad line 94
  14. theorem OAI.MeanPayoff.high_core_displacement line 98
  15. theorem OAI.MeanPayoff.low_core_displacement line 144
  16. theorem OAI.MeanPayoff.RandomTree.uniform_probability line 197
  17. theorem OAI.MeanPayoff.RandomTree.sample_badTimes line 205
  18. theorem OAI.MeanPayoff.nearHigh_child_core line 218
  19. theorem OAI.MeanPayoff.nearLow_child_core line 238
  20. def OAI.MeanPayoff.Alternative line 258
  21. def OAI.MeanPayoff.HighAlternative line 262
  22. def OAI.MeanPayoff.LowAlternative line 266
  23. theorem OAI.MeanPayoff.alternative_mono line 270
  24. theorem OAI.MeanPayoff.alternative_witness line 281