OAI/Computability/VertexCover/Fourier/FourierResponse.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.Hastad.supportResponse line 44
2. theorem OAI.UniqueGames.Foundations.Hastad.supportResponse_expectation line 57
3. def OAI.UniqueGames.Foundations.Hastad.fourierResponse line 68
4. theorem OAI.UniqueGames.Foundations.Hastad.fourierResponse_expectation line 78
5. theorem OAI.UniqueGames.Foundations.Hastad.response_expectation_nonnegative line 93
6. def OAI.UniqueGames.Foundations.Hastad.responseAgreement line 98
7. def OAI.UniqueGames.Foundations.Hastad.validResponseAgreement line 103
8. theorem OAI.UniqueGames.Foundations.Hastad.supportResponse_validAgreement line 110
9. theorem OAI.UniqueGames.Foundations.Hastad.validAgreement_le_supportResponses line 124
10. theorem OAI.UniqueGames.Foundations.Hastad.validDecoderSuccess_le_response line 150
11. theorem OAI.UniqueGames.Foundations.Hastad.conditioned_folded_response_bound line 167