OAI/Computability/VertexCover/Fourier/Decoder.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.Hastad.parityProjection line 17
2. theorem OAI.UniqueGames.Foundations.Hastad.walsh_support line 20
3. theorem OAI.UniqueGames.Foundations.Hastad.sign_power_parity line 28
4. theorem OAI.UniqueGames.Foundations.Hastad.walsh_pullback line 38
5. theorem OAI.UniqueGames.Foundations.Hastad.projectedCoefficient_eq line 48
6. theorem OAI.UniqueGames.Foundations.Hastad.projection_has_preimage line 53
7. theorem OAI.UniqueGames.Foundations.Hastad.scaled_geometric_power_le_one line 65
8. theorem OAI.UniqueGames.Foundations.Hastad.noise_decay_bound line 79
9. def OAI.UniqueGames.Foundations.Hastad.zeroMask line 92
10. theorem OAI.UniqueGames.Foundations.Hastad.support_eq_empty_iff line 95
11. theorem OAI.UniqueGames.Foundations.Hastad.parityProjection_zero line 107
12. def OAI.UniqueGames.Foundations.Hastad.agreementProbability line 112
13. theorem OAI.UniqueGames.Foundations.Hastad.agreementProbability_nonneg line 117
14. theorem OAI.UniqueGames.Foundations.Hastad.agreementProbability_projection line 125
15. def OAI.UniqueGames.Foundations.Hastad.decoderSuccess line 151
16. def OAI.UniqueGames.Foundations.Hastad.decodingEnergy line 155
17. theorem OAI.UniqueGames.Foundations.Hastad.decodingEnergy_le_success line 158
18. theorem OAI.UniqueGames.Foundations.Hastad.bias_sq_le_weighted_energy line 192
19. theorem OAI.UniqueGames.Foundations.Hastad.decoder_four_epsilon_bias_sq line 209
20. theorem OAI.UniqueGames.Foundations.Hastad.folded_decoder_bound line 235
21. def OAI.UniqueGames.Foundations.Hastad.validAgreementProbability line 243
22. theorem OAI.UniqueGames.Foundations.Hastad.validAgreementProbability_eq line 250
23. def OAI.UniqueGames.Foundations.Hastad.validDecoderSuccess line 263
24. theorem OAI.UniqueGames.Foundations.Hastad.conditioned_validDecoderSuccess line 269
25. theorem OAI.UniqueGames.Foundations.Hastad.conditioned_folded_decoder_bound line 287