OAI/Computability/MeanPayoff/WinnerCorrespondence.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.Label.transformed_ne_zero line 7
  2. def OAI.MeanPayoff.Label.sourceWeight line 17
  3. theorem OAI.MeanPayoff.Label.weightBound_eq_source line 20
  4. def OAI.MeanPayoff.Label.initialExponent line 28
  5. def OAI.MeanPayoff.Label.initialWidth line 30
  6. theorem OAI.MeanPayoff.Label.initialWidth_ge line 32
  7. theorem OAI.MeanPayoff.Label.initialExponent_least line 41
  8. theorem OAI.MeanPayoff.Label.initialWidth_large line 48
  9. theorem OAI.MeanPayoff.Label.wide_winning_iff line 54
  10. def OAI.MeanPayoff.Label.uniformMass line 103
  11. theorem OAI.MeanPayoff.Label.uniformMass_pos line 105
  12. theorem OAI.MeanPayoff.Label.uniformMass_le_one line 111
  13. theorem OAI.MeanPayoff.Label.labels_correct_of_large_width line 118
  14. theorem OAI.MeanPayoff.Label.main_labels_correct line 154
  15. def OAI.MeanPayoff.Label.mainLabels line 160
  16. theorem OAI.MeanPayoff.Label.mainLabels_correct line 164