OAI/Computability/VertexCover/Fourier/GameDecoder.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGames.Foundations.Hastad.distribution_sq_expectation_le line 40
  2. def OAI.UniqueGames.Foundations.Hastad.projectionGame line 70
  3. def OAI.UniqueGames.Foundations.Hastad.questionBias line 75
  4. def OAI.UniqueGames.Foundations.Hastad.questionAcceptance line 79
  5. theorem OAI.UniqueGames.Foundations.Hastad.questionAcceptance_eq line 84
  6. inductive OAI.UniqueGames.Foundations.Hastad.ConditionedOracle line 95
  7. def OAI.UniqueGames.Foundations.Hastad.ConditionedOracle.answer line 99
  8. def OAI.UniqueGames.Foundations.Hastad.ConditionedOracle.fallback line 103
  9. theorem OAI.UniqueGames.Foundations.Hastad.testBias_constant_right line 109
  10. theorem OAI.UniqueGames.Foundations.Hastad.empty_conditioned_bias line 116
  11. theorem OAI.UniqueGames.Foundations.Hastad.conditionedOracle_response_bound line 126
  12. theorem OAI.UniqueGames.Foundations.Hastad.folded_game_decoder_bound line 146
  13. theorem OAI.UniqueGames.Foundations.Hastad.conditionedOracle_game_decoder_bound line 184
  14. theorem OAI.UniqueGames.Foundations.Hastad.conditionedOracle_acceptance_bound line 220