OAI/Combinatorics/IndependentSets/Repetition/Value.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Games.Game.value line 18
  2. theorem OAI.IndependentSetsGames.Foundations.Games.Game.success_le_value line 22
  3. theorem OAI.IndependentSetsGames.Foundations.Games.Game.value_le_iff line 27
  4. theorem OAI.IndependentSetsGames.Foundations.Games.Game.exists_optimal_strategy line 32
  5. theorem OAI.IndependentSetsGames.Foundations.Games.Game.value_nonnegative line 39
  6. theorem OAI.IndependentSetsGames.Foundations.Games.Game.value_le_one line 44
  7. theorem OAI.IndependentSetsGames.Foundations.Games.Game.randomized_success_le_value line 47
  8. theorem OAI.IndependentSetsGames.Foundations.Games.Game.success_repetition_zero line 60
  9. theorem OAI.IndependentSetsGames.Foundations.Games.Game.value_repetition_zero line 69
  10. theorem OAI.IndependentSetsGames.Foundations.Games.Game.pow_value_le_repetition_value line 75
  11. theorem OAI.IndependentSetsGames.Foundations.Games.Game.value_le_of_localSimulation line 81
  12. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.eq_of_weight_eq line 103
  13. def OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.table line 113
  14. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.expectation_table_eval line 124
  15. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.table_eval_pushforward line 152
  16. def OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.product line 166
  17. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.expectation_product line 175
  18. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.expectation_comm line 181
  19. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.expectation_congr line 194
  20. def OAI.IndependentSetsGames.Foundations.Games.Game.responseTableLaw line 207
  21. def OAI.IndependentSetsGames.Foundations.Games.Game.stochasticSuccess line 213
  22. theorem OAI.IndependentSetsGames.Foundations.Games.Game.success_eq_question_expectation line 222
  23. theorem OAI.IndependentSetsGames.Foundations.Games.Game.table_success_eq_stochastic line 229
  24. theorem OAI.IndependentSetsGames.Foundations.Games.Game.stochasticSuccess_le_value line 267
  25. theorem OAI.IndependentSetsGames.Foundations.Games.Game.exists_deterministic_ge_stochastic line 275