OAI/Combinatorics/IndependentSets/Fourier/GameDecoder.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.Hastad.distribution_sq_expectation_le line 13
2. def OAI.IndependentSetsGames.Foundations.Hastad.projectionGame line 43
3. def OAI.IndependentSetsGames.Foundations.Hastad.questionBias line 48
4. def OAI.IndependentSetsGames.Foundations.Hastad.questionAcceptance line 52
5. theorem OAI.IndependentSetsGames.Foundations.Hastad.questionAcceptance_eq line 57
6. inductive OAI.IndependentSetsGames.Foundations.Hastad.ConditionedOracle line 68
7. def OAI.IndependentSetsGames.Foundations.Hastad.ConditionedOracle.answer line 72
8. def OAI.IndependentSetsGames.Foundations.Hastad.ConditionedOracle.fallback line 76
9. theorem OAI.IndependentSetsGames.Foundations.Hastad.testBias_constant_right line 81
10. theorem OAI.IndependentSetsGames.Foundations.Hastad.empty_conditioned_bias line 87
11. theorem OAI.IndependentSetsGames.Foundations.Hastad.conditionedOracle_response_bound line 96
12. theorem OAI.IndependentSetsGames.Foundations.Hastad.folded_game_decoder_bound line 118
13. theorem OAI.IndependentSetsGames.Foundations.Hastad.conditionedOracle_game_decoder_bound line 156
14. theorem OAI.IndependentSetsGames.Foundations.Hastad.conditionedOracle_acceptance_bound line 192