OAI/Computability/MeanPayoff/Deviation.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.deviation line 9
  2. theorem OAI.MeanPayoff.le_deviation line 12
  3. theorem OAI.MeanPayoff.deviation_le line 16
  4. theorem OAI.MeanPayoff.deviation_attained line 20
  5. def OAI.MeanPayoff.highCore line 27
  6. def OAI.MeanPayoff.lowCore line 30
  7. def OAI.MeanPayoff.nearHigh line 34
  8. def OAI.MeanPayoff.nearLow line 36
  9. theorem OAI.MeanPayoff.SolveBox.radius_bounds line 41
  10. theorem OAI.MeanPayoff.SolveBox.midpoint_twice line 62
  11. theorem OAI.MeanPayoff.SolveBox.average_movement line 69
  12. theorem OAI.MeanPayoff.highCore_support line 87
  13. theorem OAI.MeanPayoff.lowCore_support line 96
  14. theorem OAI.MeanPayoff.high_initial_deficit line 105
  15. theorem OAI.MeanPayoff.low_initial_deficit line 125
  16. theorem OAI.MeanPayoff.high_center_deviation line 145
  17. theorem OAI.MeanPayoff.low_center_deviation line 167
  18. theorem OAI.MeanPayoff.RandomTree.probability_leaf line 194
  19. theorem OAI.MeanPayoff.RandomTree.probability_zero_of_all line 199
  20. theorem OAI.MeanPayoff.RandomTree.bind_error line 207
  21. theorem OAI.MeanPayoff.RandomTree.bind_probability_le line 227
  22. theorem OAI.MeanPayoff.RandomTree.map_error line 235
  23. def OAI.MeanPayoff.Comparisons line 245
  24. def OAI.MeanPayoff.LowerComparisons line 252
  25. theorem OAI.MeanPayoff.centered_active_high line 256
  26. theorem OAI.MeanPayoff.centered_active_low line 263
  27. theorem OAI.MeanPayoff.centered_admissible_high line 270
  28. theorem OAI.MeanPayoff.centered_admissible_low line 287