OAI/Computability/RandomMean/Realizer.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.Realizer.preTail line 8
  2. def OAI.MeanPayoff.Realizer.pre line 9
  3. def OAI.MeanPayoff.Realizer.preCost line 10
  4. theorem OAI.MeanPayoff.Realizer.pre_quiet line 12
  5. theorem OAI.MeanPayoff.Realizer.pre_runs line 14
  6. def OAI.MeanPayoff.Realizer.post line 26
  7. def OAI.MeanPayoff.Realizer.postCost line 27
  8. theorem OAI.MeanPayoff.Realizer.post_quiet line 28
  9. theorem OAI.MeanPayoff.Realizer.post_runs line 29
  10. theorem OAI.MeanPayoff.Realizer.digits_length line 37
  11. theorem OAI.MeanPayoff.Realizer.post_polynomial line 41
  12. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.halted_value line 56
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.loop_expect line 70
  14. theorem OAI.MeanPayoff.SourceControl.root_rank line 90
  15. theorem OAI.MeanPayoff.Realizer.classify_rep line 99
  16. theorem OAI.MeanPayoff.Realizer.root_loop_law line 107
  17. def OAI.MeanPayoff.Realizer.program line 128
  18. def OAI.MeanPayoff.Realizer.aux line 129
  19. def OAI.MeanPayoff.Realizer.amount line 130
  20. def OAI.MeanPayoff.Realizer.answer line 131
  21. theorem OAI.MeanPayoff.Realizer.pre_cost_bound line 132
  22. theorem OAI.MeanPayoff.Realizer.amount_bound line 140
  23. theorem OAI.MeanPayoff.Realizer.aux_bound line 142
  24. def OAI.MeanPayoff.Realizer.postBudget line 144
  25. theorem OAI.MeanPayoff.Realizer.input_size line 146
  26. theorem OAI.MeanPayoff.Realizer.post_budget line 152
  27. theorem OAI.MeanPayoff.Realizer.budget_bound line 161
  28. def OAI.MeanPayoff.Realizer.limit line 164
  29. theorem OAI.MeanPayoff.Realizer.limit_bound line 165
  30. theorem OAI.MeanPayoff.Realizer.trace line 167