OAI/Computability/VertexCover/Fourier/SourceGame.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.event_nonempty line 47
  2. def OAI.UniqueGames.Foundations.Hastad.SourceGame.eventLaw line 51
  3. def OAI.UniqueGames.Foundations.Hastad.SourceGame.visibleQuestion line 56
  4. def OAI.UniqueGames.Foundations.Hastad.SourceGame.baseGame line 60
  5. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.baseGame_accepts line 65
  6. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.eventLaw_probability line 69
  7. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.sum_slots line 82
  8. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.sum_slot_accepts line 92
  9. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.failureCount_eq_sum_map line 106
  10. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.failureCount_allIndices line 114
  11. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.verifier_probability_plus_failure line 121
  12. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.base_success_le_verifier line 142
  13. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.base_value_le_of_clause_gap line 152
  14. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.pushforward_comp line 172
  15. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.expectation_pushforward line 187
  16. def OAI.UniqueGames.Foundations.Hastad.SourceGame.repeatedVisible line 198
  17. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.repeated_questions line 203
  18. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.repeated_expectation line 212
  19. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.repeated_expectation_split line 223
  20. def OAI.UniqueGames.Foundations.Hastad.SourceGame.sourceProjectionGame line 237
  21. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.projection_value_le_repetition line 242
  22. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.source_acceptance_le line 261
  23. theorem OAI.UniqueGames.Foundations.Hastad.SourceGame.source_acceptance_le_split line 276