OAI/Computability/VertexCover/Games/Stochastic.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.eq_of_weight_eq line 39
  2. def OAI.UniqueGames.Foundations.Games.FiniteDistribution.table line 49
  3. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.expectation_table_eval line 60
  4. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.table_eval_pushforward line 88
  5. def OAI.UniqueGames.Foundations.Games.FiniteDistribution.product line 102
  6. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.expectation_product line 111
  7. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.expectation_comm line 117
  8. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.expectation_congr line 130
  9. def OAI.UniqueGames.Foundations.Games.Game.responseTableLaw line 143
  10. def OAI.UniqueGames.Foundations.Games.Game.stochasticSuccess line 149
  11. theorem OAI.UniqueGames.Foundations.Games.Game.success_eq_question_expectation line 158
  12. theorem OAI.UniqueGames.Foundations.Games.Game.table_success_eq_stochastic line 165
  13. theorem OAI.UniqueGames.Foundations.Games.Game.stochasticSuccess_le_value line 203
  14. theorem OAI.UniqueGames.Foundations.Games.Game.exists_deterministic_ge_stochastic line 211