OAI/Combinatorics/IndependentSets/Fourier/Game.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.event_nonempty line 15
  2. def OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.eventLaw line 19
  3. def OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.visibleQuestion line 24
  4. def OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.baseGame line 28
  5. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.baseGame_accepts line 33
  6. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.eventLaw_probability line 37
  7. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.sum_slots line 50
  8. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.sum_slot_accepts line 60
  9. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.failureCount_eq_sum_map line 74
  10. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.failureCount_allIndices line 82
  11. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.verifier_probability_plus_failure line 89
  12. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.base_success_le_verifier line 110
  13. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.base_value_le_of_clause_gap line 120
  14. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.pushforward_comp line 140
  15. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.expectation_pushforward line 155
  16. def OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.repeatedVisible line 166
  17. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.repeated_questions line 171
  18. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.repeated_expectation line 180
  19. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.repeated_expectation_split line 191
  20. def OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.sourceProjectionGame line 205
  21. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.projection_value_le_repetition line 210
  22. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.source_acceptance_le line 229
  23. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceGame.source_acceptance_le_split line 244