OAI/Computability/MeanPayoff/CountedTraversal.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.admissible_bottom line 9
  2. theorem OAI.MeanPayoff.admissible_top line 14
  3. theorem OAI.MeanPayoff.solve_comparisons line 19
  4. def OAI.MeanPayoff.rootBudgets line 48
  5. theorem OAI.MeanPayoff.rootBudgets_parameter line 58
  6. theorem OAI.MeanPayoff.topWidth_positive line 62
  7. def OAI.MeanPayoff.rootBox line 66
  8. theorem OAI.MeanPayoff.root_sub_admissible line 75
  9. theorem OAI.MeanPayoff.root_super_admissible line 83
  10. theorem OAI.MeanPayoff.solve_root_exact line 91
  11. def OAI.MeanPayoff.gameSolve line 111
  12. def OAI.MeanPayoff.CorrectSet line 114
  13. theorem OAI.MeanPayoff.gameSolve_failure line 116
  14. theorem OAI.MeanPayoff.gameSolve_success line 129
  15. theorem OAI.MeanPayoff.RandomTree.leaf_bind line 138
  16. theorem OAI.MeanPayoff.RandomTree.bind_leaf line 141
  17. theorem OAI.MeanPayoff.RandomTree.bind_assoc line 146
  18. theorem OAI.MeanPayoff.RandomTree.map_map line 153
  19. theorem OAI.MeanPayoff.RandomTree.bind_map line 156
  20. theorem OAI.MeanPayoff.RandomTree.all_map line 160
  21. structure OAI.MeanPayoff.Counted line 166
  22. def OAI.MeanPayoff.Counted.pure line 171
  23. def OAI.MeanPayoff.Counted.lift line 172
  24. def OAI.MeanPayoff.Counted.map line 173
  25. def OAI.MeanPayoff.Counted.bind line 175
  26. def OAI.MeanPayoff.Counted.charge line 177
  27. def OAI.MeanPayoff.Counted.erase line 179
  28. def OAI.MeanPayoff.Counted.Bounded line 180
  29. theorem OAI.MeanPayoff.Counted.erase_pure line 182
  30. theorem OAI.MeanPayoff.Counted.erase_lift line 183
  31. theorem OAI.MeanPayoff.Counted.erase_map line 185
  32. theorem OAI.MeanPayoff.Counted.erase_bind line 187
  33. theorem OAI.MeanPayoff.Counted.erase_charge line 190
  34. theorem OAI.MeanPayoff.Counted.bounded_pure line 193
  35. theorem OAI.MeanPayoff.Counted.bounded_lift line 195
  36. theorem OAI.MeanPayoff.Counted.bounded_mono line 199
  37. theorem OAI.MeanPayoff.Counted.bounded_map line 202
  38. theorem OAI.MeanPayoff.Counted.bounded_charge line 205
  39. theorem OAI.MeanPayoff.Counted.bounded_bind line 210
  40. theorem OAI.MeanPayoff.Counted.bounded_bind_qualified line 219
  41. def OAI.MeanPayoff.Counted.trials line 230
  42. def OAI.MeanPayoff.Counted.traverse line 234
  43. theorem OAI.MeanPayoff.Counted.erase_trials line 238
  44. theorem OAI.MeanPayoff.Counted.erase_traverse line 244
  45. theorem OAI.MeanPayoff.Counted.bounded_trials line 250
  46. theorem OAI.MeanPayoff.Counted.bounded_traverse line 258