OAI/Computability/VertexCover/Games/Basic.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniqueGames.Foundations.Games.FiniteDistribution line 37
  2. def OAI.UniqueGames.Foundations.Games.FiniteDistribution.expectation line 46
  3. def OAI.UniqueGames.Foundations.Games.FiniteDistribution.probability line 49
  4. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.probability_nonnegative line 52
  5. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.probability_le_one line 60
  6. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.probability_true line 69
  7. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.probability_false line 73
  8. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.probability_mono line 77
  9. def OAI.UniqueGames.Foundations.Games.FiniteDistribution.pushforward line 89
  10. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.probability_pushforward line 101
  11. def OAI.UniqueGames.Foundations.Games.FiniteDistribution.transport line 113
  12. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.probability_transport line 118
  13. def OAI.UniqueGames.Foundations.Games.FiniteDistribution.iid line 124
  14. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.probability_iid_all line 129
  15. abbrev OAI.UniqueGames.Foundations.Games.Strategy line 148
  16. structure OAI.UniqueGames.Foundations.Games.Game line 150
  17. def OAI.UniqueGames.Foundations.Games.Game.wins line 160
  18. def OAI.UniqueGames.Foundations.Games.Game.success line 164
  19. theorem OAI.UniqueGames.Foundations.Games.Game.success_nonnegative line 167
  20. theorem OAI.UniqueGames.Foundations.Games.Game.success_le_one line 171
  21. def OAI.UniqueGames.Foundations.Games.Game.simulatedStrategy line 175
  22. theorem OAI.UniqueGames.Foundations.Games.Game.success_le_of_localSimulation line 182
  23. def OAI.UniqueGames.Foundations.Games.Game.tupleQuestionEquiv line 201
  24. def OAI.UniqueGames.Foundations.Games.Game.repetition line 208
  25. def OAI.UniqueGames.Foundations.Games.Game.repeatStrategy line 215
  26. theorem OAI.UniqueGames.Foundations.Games.Game.success_repeatStrategy line 219
  27. theorem OAI.UniqueGames.Foundations.Games.Game.repetition_question_weight line 227
  28. theorem OAI.UniqueGames.Foundations.Games.Game.repetition_accepts_iff line 232
  29. def OAI.UniqueGames.Foundations.Games.Game.coordinateWin line 239
  30. def OAI.UniqueGames.Foundations.Games.Game.selectedWins line 245
  31. theorem OAI.UniqueGames.Foundations.Games.Game.selectedWins_mono line 251
  32. theorem OAI.UniqueGames.Foundations.Games.Game.selectedWins_empty line 262
  33. theorem OAI.UniqueGames.Foundations.Games.Game.selectedWins_univ line 268