OAI/Combinatorics/IndependentSets/Repetition/Basic.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution line 11
  2. def OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.expectation line 20
  3. def OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability line 23
  4. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_nonnegative line 26
  5. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_le_one line 34
  6. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_true line 43
  7. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_false line 47
  8. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_mono line 51
  9. def OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.pushforward line 63
  10. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_pushforward line 75
  11. def OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.transport line 87
  12. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_transport line 92
  13. def OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.iid line 98
  14. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_iid_all line 103
  15. abbrev OAI.IndependentSetsGames.Foundations.Games.Strategy line 122
  16. structure OAI.IndependentSetsGames.Foundations.Games.Game line 124
  17. def OAI.IndependentSetsGames.Foundations.Games.Game.wins line 134
  18. def OAI.IndependentSetsGames.Foundations.Games.Game.success line 138
  19. theorem OAI.IndependentSetsGames.Foundations.Games.Game.success_nonnegative line 141
  20. theorem OAI.IndependentSetsGames.Foundations.Games.Game.success_le_one line 145
  21. def OAI.IndependentSetsGames.Foundations.Games.Game.simulatedStrategy line 149
  22. theorem OAI.IndependentSetsGames.Foundations.Games.Game.success_le_of_localSimulation line 156
  23. def OAI.IndependentSetsGames.Foundations.Games.Game.tupleQuestionEquiv line 175
  24. def OAI.IndependentSetsGames.Foundations.Games.Game.repetition line 182
  25. def OAI.IndependentSetsGames.Foundations.Games.Game.repeatStrategy line 189
  26. theorem OAI.IndependentSetsGames.Foundations.Games.Game.success_repeatStrategy line 193
  27. theorem OAI.IndependentSetsGames.Foundations.Games.Game.repetition_question_weight line 201
  28. theorem OAI.IndependentSetsGames.Foundations.Games.Game.repetition_accepts_iff line 206
  29. def OAI.IndependentSetsGames.Foundations.Games.Game.coordinateWin line 213
  30. def OAI.IndependentSetsGames.Foundations.Games.Game.selectedWins line 219
  31. theorem OAI.IndependentSetsGames.Foundations.Games.Game.selectedWins_mono line 225
  32. theorem OAI.IndependentSetsGames.Foundations.Games.Game.selectedWins_empty line 236
  33. theorem OAI.IndependentSetsGames.Foundations.Games.Game.selectedWins_univ line 242