OAI/Computability/RandomMean/Complexity.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.Realizer.iterations line 8
  2. theorem OAI.MeanPayoff.Realizer.iterations_bound line 9
  3. theorem OAI.MeanPayoff.Realizer.root_game line 12
  4. theorem OAI.MeanPayoff.Realizer.aux_game line 16
  5. theorem OAI.MeanPayoff.Realizer.amount_game line 22
  6. theorem OAI.MeanPayoff.Realizer.answer_eval line 26
  7. theorem OAI.MeanPayoff.Realizer.answer_game line 30
  8. theorem OAI.MeanPayoff.Realizer.answer_expect line 42
  9. def OAI.MeanPayoff.Realizer.total line 67
  10. theorem OAI.MeanPayoff.Realizer.total_formula line 69
  11. theorem OAI.MeanPayoff.Realizer.total_bound line 74
  12. theorem OAI.MeanPayoff.Realizer.resource_quasi line 82
  13. theorem OAI.MeanPayoff.Realizer.polynomial_quasi line 105
  14. theorem OAI.MeanPayoff.Realizer.natural_quasi_real line 124
  15. theorem OAI.MeanPayoff.Realizer.total_quasi line 140
  16. theorem OAI.MeanPayoff.Realizer.tree_halts line 151
  17. theorem OAI.MeanPayoff.Realizer.tree_answer line 155
  18. theorem OAI.MeanPayoff.Realizer.tree_law line 162
  19. theorem OAI.MeanPayoff.Realizer.tree_success line 167