OAI/Computability/MinUncut/PCP/FourierResponse.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Hastad.supportResponse line 19
2. theorem OAI.MinUncutGames.Foundations.Hastad.supportResponse_expectation line 32
3. def OAI.MinUncutGames.Foundations.Hastad.fourierResponse line 43
4. theorem OAI.MinUncutGames.Foundations.Hastad.fourierResponse_expectation line 53
5. theorem OAI.MinUncutGames.Foundations.Hastad.response_expectation_nonnegative line 68
6. def OAI.MinUncutGames.Foundations.Hastad.responseAgreement line 73
7. def OAI.MinUncutGames.Foundations.Hastad.validResponseAgreement line 78
8. theorem OAI.MinUncutGames.Foundations.Hastad.supportResponse_validAgreement line 85
9. theorem OAI.MinUncutGames.Foundations.Hastad.validAgreement_le_supportResponses line 99
10. theorem OAI.MinUncutGames.Foundations.Hastad.validDecoderSuccess_le_response line 125
11. theorem OAI.MinUncutGames.Foundations.Hastad.conditioned_folded_response_bound line 142