OAI/Computability/MeanPayoff/Pivots.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.Label.MaxClaim line 13
  2. def OAI.MeanPayoff.Label.MinClaim line 16
  3. def OAI.MeanPayoff.Label.MaxWitness line 19
  4. def OAI.MeanPayoff.Label.MinWitness line 23
  5. def OAI.MeanPayoff.Label.Good line 27
  6. def OAI.MeanPayoff.Label.peak line 32
  7. def OAI.MeanPayoff.Label.gap line 35
  8. def OAI.MeanPayoff.Label.near line 38
  9. theorem OAI.MeanPayoff.Label.le_peak line 41
  10. theorem OAI.MeanPayoff.Label.peak_le line 45
  11. theorem OAI.MeanPayoff.Label.peak_attained line 49
  12. theorem OAI.MeanPayoff.Label.gap_nonneg line 55
  13. theorem OAI.MeanPayoff.Label.centerSub_of_support line 58
  14. theorem OAI.MeanPayoff.Label.centerSuper_of_support line 98
  15. theorem OAI.MeanPayoff.Label.centerSub_active line 138
  16. theorem OAI.MeanPayoff.Label.centerSuper_active line 147
  17. theorem OAI.MeanPayoff.Label.centerSub_claim line 156
  18. theorem OAI.MeanPayoff.Label.centerSuper_claim line 163
  19. theorem OAI.MeanPayoff.Label.max_outside_gap line 170
  20. theorem OAI.MeanPayoff.Label.min_outside_gap line 185
  21. theorem OAI.MeanPayoff.Label.translate_max line 200
  22. theorem OAI.MeanPayoff.Label.translate_min line 217
  23. theorem OAI.MeanPayoff.Label.mass_scale line 234
  24. theorem OAI.MeanPayoff.Label.translate_max_witness line 238
  25. theorem OAI.MeanPayoff.Label.translate_min_witness line 257
  26. def OAI.MeanPayoff.Label.downStep line 276
  27. def OAI.MeanPayoff.Label.upStep line 280
  28. theorem OAI.MeanPayoff.Label.downStep_bounds line 284
  29. theorem OAI.MeanPayoff.Label.upStep_bounds line 293
  30. theorem OAI.MeanPayoff.Label.downStep_peak line 302
  31. theorem OAI.MeanPayoff.Label.upStep_peak line 323
  32. theorem OAI.MeanPayoff.Label.down_protection line 344
  33. theorem OAI.MeanPayoff.Label.up_protection line 365
  34. theorem OAI.MeanPayoff.Label.down_stationary_heavy line 386
  35. theorem OAI.MeanPayoff.Label.up_stationary_heavy line 416
  36. theorem OAI.MeanPayoff.Label.near_mono_up line 446
  37. theorem OAI.MeanPayoff.Label.max_mark_safe line 455
  38. theorem OAI.MeanPayoff.Label.min_mark_safe line 462
  39. def OAI.MeanPayoff.Label.reweight line 469
  40. theorem OAI.MeanPayoff.Label.reweight_pos line 472
  41. theorem OAI.MeanPayoff.Label.reweight_mass line 477
  42. theorem OAI.MeanPayoff.Label.reweight_survives line 487
  43. theorem OAI.MeanPayoff.Label.provisional_max_labels line 499
  44. theorem OAI.MeanPayoff.Label.provisional_min_labels line 520
  45. def OAI.MeanPayoff.Label.override line 541
  46. theorem OAI.MeanPayoff.Label.max_survives line 545
  47. theorem OAI.MeanPayoff.Label.min_survives line 560
  48. theorem OAI.MeanPayoff.Label.override_good line 577
  49. theorem OAI.MeanPayoff.Label.budget_exists line 617
  50. def OAI.MeanPayoff.Label.budget line 630
  51. theorem OAI.MeanPayoff.Label.budget_spec line 633
  52. theorem OAI.MeanPayoff.Label.budget_zero_iff line 637
  53. theorem OAI.MeanPayoff.Label.budget_decreases line 641
  54. theorem OAI.MeanPayoff.Label.reweight_product line 663