OAI/Computability/MeanPayoff/FiniteBox.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MeanPayoff.Vec line 8
  2. def OAI.MeanPayoff.shift line 10
  3. def OAI.MeanPayoff.clip line 12
  4. def OAI.MeanPayoff.InBox line 15
  5. def OAI.MeanPayoff.Subsolution line 17
  6. def OAI.MeanPayoff.Supersolution line 20
  7. def OAI.MeanPayoff.subSupport line 23
  8. def OAI.MeanPayoff.superSupport line 24
  9. structure OAI.MeanPayoff.OperatorLaws line 26
  10. def OAI.MeanPayoff.transformed line 30
  11. def OAI.MeanPayoff.outgoing line 32
  12. theorem OAI.MeanPayoff.outgoing_nonempty line 35
  13. def OAI.MeanPayoff.operator line 39
  14. theorem OAI.MeanPayoff.operator_laws line 45
  15. theorem OAI.MeanPayoff.subsolution_raise_floor line 78
  16. theorem OAI.MeanPayoff.supersolution_lower_ceiling line 96
  17. def OAI.MeanPayoff.centerSub line 114
  18. def OAI.MeanPayoff.centerSuper line 117
  19. theorem OAI.MeanPayoff.centerSub_support line 120
  20. theorem OAI.MeanPayoff.centerSuper_support line 128
  21. theorem OAI.MeanPayoff.centered_subsolution line 136
  22. theorem OAI.MeanPayoff.centered_supersolution line 172
  23. def OAI.MeanPayoff.averageStep line 210
  24. theorem OAI.MeanPayoff.high_deviation_step line 213
  25. theorem OAI.MeanPayoff.high_bad_step line 230
  26. theorem OAI.MeanPayoff.low_deviation_step line 244
  27. theorem OAI.MeanPayoff.low_bad_step line 261
  28. theorem OAI.MeanPayoff.no_tight_sequence line 275
  29. theorem OAI.MeanPayoff.comparison_step line 304
  30. theorem OAI.MeanPayoff.box_comparison line 344
  31. def OAI.MeanPayoff.boxStep line 373
  32. theorem OAI.MeanPayoff.boxStep_in_box line 376
  33. theorem OAI.MeanPayoff.boxStep_mono line 383
  34. theorem OAI.MeanPayoff.fixed_iff_comparisons line 388
  35. def OAI.MeanPayoff.volume line 414
  36. theorem OAI.MeanPayoff.volume_decreases line 416
  37. def OAI.MeanPayoff.basicFrom line 429
  38. def OAI.MeanPayoff.basic line 446
  39. theorem OAI.MeanPayoff.basic_spec line 450
  40. theorem OAI.MeanPayoff.box_solution_exists_unique line 459
  41. theorem OAI.MeanPayoff.no_tight_segment line 468
  42. theorem OAI.MeanPayoff.operator_attained line 498
  43. theorem OAI.MeanPayoff.solution_near_boundary line 508
  44. theorem OAI.MeanPayoff.exists_rounding_shift line 573
  45. theorem OAI.MeanPayoff.rounded_high_edge line 603
  46. def OAI.MeanPayoff.weightBound line 619
  47. def OAI.MeanPayoff.topWidth line 622
  48. theorem OAI.MeanPayoff.weightBound_positive line 624
  49. theorem OAI.MeanPayoff.transformed_le_bound line 629
  50. theorem OAI.MeanPayoff.top_bands line 636
  51. theorem OAI.MeanPayoff.max_edge_le_operator line 646
  52. theorem OAI.MeanPayoff.operator_le_min_edge line 652
  53. theorem OAI.MeanPayoff.move_tail line 658
  54. theorem OAI.MeanPayoff.next_position line 665
  55. theorem OAI.MeanPayoff.high_edge_stays_high line 668
  56. theorem OAI.MeanPayoff.low_edge_stays_low line 682
  57. theorem OAI.MeanPayoff.high_strategy line 696
  58. theorem OAI.MeanPayoff.low_strategy line 732
  59. def OAI.MeanPayoff.vectorBound line 768
  60. theorem OAI.MeanPayoff.le_vectorBound line 771
  61. def OAI.MeanPayoff.average line 777
  62. theorem OAI.MeanPayoff.average_bounds line 779
  63. theorem OAI.MeanPayoff.payoff_bounded line 796
  64. theorem OAI.MeanPayoff.lower_average_from_potential line 811
  65. theorem OAI.MeanPayoff.upper_average_from_potential line 823
  66. theorem OAI.MeanPayoff.high_payoff line 850
  67. theorem OAI.MeanPayoff.low_payoff line 882
  68. theorem OAI.MeanPayoff.winning_iff_high line 917
  69. def OAI.MeanPayoff.mass line 947
  70. def OAI.MeanPayoff.lowerActive line 949
  71. def OAI.MeanPayoff.upperActive line 952
  72. theorem OAI.MeanPayoff.mass_nonneg line 955
  73. theorem OAI.MeanPayoff.mass_mono line 958
  74. theorem OAI.MeanPayoff.weight_le_mass line 962