OAI/Computability/BinPacking/Games/Reindexing.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingGames.Foundations.Games.FiniteDistribution line 19
  2. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.expectation line 28
  3. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability line 31
  4. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_nonnegative line 34
  5. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_le_one line 42
  6. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_true line 51
  7. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_false line 55
  8. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_mono line 59
  9. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.pushforward line 71
  10. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_pushforward line 83
  11. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.transport line 95
  12. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_transport line 100
  13. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.iid line 106
  14. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_iid_all line 111
  15. abbrev OAI.BinPackingGames.Foundations.Games.Strategy line 130
  16. structure OAI.BinPackingGames.Foundations.Games.Game line 132
  17. def OAI.BinPackingGames.Foundations.Games.Game.wins line 144
  18. def OAI.BinPackingGames.Foundations.Games.Game.success line 148
  19. theorem OAI.BinPackingGames.Foundations.Games.Game.success_nonnegative line 151
  20. theorem OAI.BinPackingGames.Foundations.Games.Game.success_le_one line 155
  21. def OAI.BinPackingGames.Foundations.Games.Game.simulatedStrategy line 159
  22. theorem OAI.BinPackingGames.Foundations.Games.Game.success_le_of_localSimulation line 166
  23. def OAI.BinPackingGames.Foundations.Games.Game.tupleQuestionEquiv line 185
  24. def OAI.BinPackingGames.Foundations.Games.Game.repetition line 192
  25. def OAI.BinPackingGames.Foundations.Games.Game.repeatStrategy line 199
  26. theorem OAI.BinPackingGames.Foundations.Games.Game.success_repeatStrategy line 203
  27. theorem OAI.BinPackingGames.Foundations.Games.Game.repetition_question_weight line 211
  28. theorem OAI.BinPackingGames.Foundations.Games.Game.repetition_accepts_iff line 216
  29. def OAI.BinPackingGames.Foundations.Games.Game.coordinateWin line 223
  30. def OAI.BinPackingGames.Foundations.Games.Game.selectedWins line 229
  31. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedWins_mono line 235
  32. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedWins_empty line 246
  33. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedWins_univ line 252
  34. def OAI.BinPackingGames.Foundations.Games.Game.value line 265
  35. theorem OAI.BinPackingGames.Foundations.Games.Game.success_le_value line 269
  36. theorem OAI.BinPackingGames.Foundations.Games.Game.value_le_iff line 274
  37. theorem OAI.BinPackingGames.Foundations.Games.Game.exists_optimal_strategy line 279
  38. theorem OAI.BinPackingGames.Foundations.Games.Game.value_nonnegative line 286
  39. theorem OAI.BinPackingGames.Foundations.Games.Game.value_le_one line 291
  40. theorem OAI.BinPackingGames.Foundations.Games.Game.randomized_success_le_value line 294
  41. theorem OAI.BinPackingGames.Foundations.Games.Game.success_repetition_zero line 307
  42. theorem OAI.BinPackingGames.Foundations.Games.Game.value_repetition_zero line 316
  43. theorem OAI.BinPackingGames.Foundations.Games.Game.pow_value_le_repetition_value line 322
  44. theorem OAI.BinPackingGames.Foundations.Games.Game.value_le_of_localSimulation line 328
  45. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.mixture line 357
  46. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_mixture line 367
  47. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_mixture_le line 384
  48. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.totalVariation line 401
  49. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.totalVariation_nonnegative line 404
  50. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.totalVariation_comm line 408
  51. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_sub_le_totalVariation line 416
  52. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_abs_sub_le_totalVariation line 432
  53. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_le_add_totalVariation line 442
  54. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.condition line 458
  55. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_condition line 474
  56. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_inter_eq_mul_conditional line 483
  57. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_and_le_left line 491
  58. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_and_le_right line 498
  59. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_and_eq_zero_of_probability_eq_zero line 505
  60. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_condition_given line 512
  61. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedWins_insert line 526
  62. def OAI.BinPackingGames.Foundations.Games.Game.selectedSuccess line 537
  63. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedSuccess_nonnegative line 542
  64. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedSuccess_le_one line 547
  65. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedSuccess_empty line 552
  66. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedSuccess_univ line 559
  67. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedSuccess_antitone line 565
  68. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedSuccess_insert line 571
  69. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedSuccess_insert_eq_zero line 583
  70. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.eq_of_weight_eq line 597
  71. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.table line 607
  72. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.expectation_table_eval line 618
  73. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.table_eval_pushforward line 646
  74. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.product line 660
  75. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.expectation_product line 669
  76. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.expectation_comm line 675
  77. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.expectation_congr line 688
  78. def OAI.BinPackingGames.Foundations.Games.Game.responseTableLaw line 701
  79. def OAI.BinPackingGames.Foundations.Games.Game.stochasticSuccess line 707
  80. theorem OAI.BinPackingGames.Foundations.Games.Game.success_eq_question_expectation line 716
  81. theorem OAI.BinPackingGames.Foundations.Games.Game.table_success_eq_stochastic line 723
  82. theorem OAI.BinPackingGames.Foundations.Games.Game.stochasticSuccess_le_value line 761
  83. theorem OAI.BinPackingGames.Foundations.Games.Game.exists_deterministic_ge_stochastic line 769
  84. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.iid_pushforward line 784
  85. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.uniform line 804
  86. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.iid_uniform line 813
  87. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.expectation_uniform line 820
  88. def OAI.BinPackingGames.Foundations.Games.FiniteDistribution.reindexEquiv line 834
  89. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.pushforward_equiv line 840
  90. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.table_const_reindex line 858
  91. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.iid_reindex line 871
  92. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.probability_reindex_of_weight line 882
  93. def OAI.BinPackingGames.Foundations.Games.Game.questionReindexEquiv line 901
  94. def OAI.BinPackingGames.Foundations.Games.Game.reindexStrategy line 906
  95. theorem OAI.BinPackingGames.Foundations.Games.Game.repetition_question_weight_reindex line 912
  96. theorem OAI.BinPackingGames.Foundations.Games.Game.repetition_questions_reindex line 923
  97. theorem OAI.BinPackingGames.Foundations.Games.Game.coordinateWin_reindex line 936
  98. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedWins_reindex line 954
  99. theorem OAI.BinPackingGames.Foundations.Games.Game.selectedSuccess_reindex line 974
  100. theorem OAI.BinPackingGames.Foundations.Games.Game.repetition_success_reindex line 989