OAI/Combinatorics/IndependentSets/Fourier/FourierResponse.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Hastad.supportResponse line 18
2. theorem OAI.IndependentSetsGames.Foundations.Hastad.supportResponse_expectation line 31
3. def OAI.IndependentSetsGames.Foundations.Hastad.fourierResponse line 42
4. theorem OAI.IndependentSetsGames.Foundations.Hastad.fourierResponse_expectation line 52
5. theorem OAI.IndependentSetsGames.Foundations.Hastad.response_expectation_nonnegative line 67
6. def OAI.IndependentSetsGames.Foundations.Hastad.responseAgreement line 72
7. def OAI.IndependentSetsGames.Foundations.Hastad.validResponseAgreement line 77
8. theorem OAI.IndependentSetsGames.Foundations.Hastad.supportResponse_validAgreement line 84
9. theorem OAI.IndependentSetsGames.Foundations.Hastad.validAgreement_le_supportResponses line 98
10. theorem OAI.IndependentSetsGames.Foundations.Hastad.validDecoderSuccess_le_response line 124
11. theorem OAI.IndependentSetsGames.Foundations.Hastad.conditioned_folded_response_bound line 141