OAI/Computability/MeanPayoff/Orientation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.high_core_exact_half line 10
  2. theorem OAI.MeanPayoff.low_core_exact_half line 28
  3. theorem OAI.MeanPayoff.orientBase_high line 45
  4. theorem OAI.MeanPayoff.orientBase_low line 56
  5. theorem OAI.MeanPayoff.core_nonempty line 68
  6. theorem OAI.MeanPayoff.orient_high_support_transfer line 75
  7. theorem OAI.MeanPayoff.orient_low_support_transfer line 89
  8. theorem OAI.MeanPayoff.RandomTree.failure_zero line 108
  9. theorem OAI.MeanPayoff.orientationTail_high line 112
  10. theorem OAI.MeanPayoff.orientationTail_low line 171
  11. def OAI.MeanPayoff.orientationError line 234
  12. theorem OAI.MeanPayoff.orientationError_nonneg line 237
  13. theorem OAI.MeanPayoff.clog_double_decrease line 241
  14. theorem OAI.MeanPayoff.orientation_error_step line 252
  15. theorem OAI.MeanPayoff.RandomTree.failure_with_metadata line 268
  16. theorem OAI.MeanPayoff.orient_high_bound line 274
  17. theorem OAI.MeanPayoff.orient_low_bound line 328