OAI/Combinatorics/IndependentSets/Fourier/Folding.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Hastad.cubeFlip line 15
2. theorem OAI.IndependentSetsGames.Foundations.Hastad.cubeFlip_cubeFlip line 18
3. theorem OAI.IndependentSetsGames.Foundations.Hastad.bitSign_not line 22
4. theorem OAI.IndependentSetsGames.Foundations.Hastad.sum_cubeFlip line 25
5. theorem OAI.IndependentSetsGames.Foundations.Hastad.coefficient_zero_of_odd line 37
6. theorem OAI.IndependentSetsGames.Foundations.Hastad.coefficient_sign_zero_of_folded line 46
7. def OAI.IndependentSetsGames.Foundations.Hastad.representative line 53
8. theorem OAI.IndependentSetsGames.Foundations.Hastad.representative_at line 57
9. theorem OAI.IndependentSetsGames.Foundations.Hastad.representative_flip line 62
10. abbrev OAI.IndependentSetsGames.Foundations.Hastad.HalfCube line 66
11. def OAI.IndependentSetsGames.Foundations.Hastad.canonicalInput line 68
12. theorem OAI.IndependentSetsGames.Foundations.Hastad.canonicalInput_flip line 72
13. def OAI.IndependentSetsGames.Foundations.Hastad.foldedAnswer line 77
14. theorem OAI.IndependentSetsGames.Foundations.Hastad.foldedAnswer_flip line 81
15. theorem OAI.IndependentSetsGames.Foundations.Hastad.foldedAnswer_zero_coefficient line 89
16. theorem OAI.IndependentSetsGames.Foundations.Hastad.foldedAnswer_dictator line 94
17. def OAI.IndependentSetsGames.Foundations.Hastad.coordinateMask line 99
18. def OAI.IndependentSetsGames.Foundations.Hastad.cubeToggle line 101
19. theorem OAI.IndependentSetsGames.Foundations.Hastad.cubeToggle_twice line 105
20. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_coordinateMask line 111
21. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_cubeToggle line 121
22. theorem OAI.IndependentSetsGames.Foundations.Hastad.sum_cubeToggle line 126
23. def OAI.IndependentSetsGames.Foundations.Hastad.restrictQuery line 139
24. theorem OAI.IndependentSetsGames.Foundations.Hastad.restrictQuery_cubeToggle line 143
25. theorem OAI.IndependentSetsGames.Foundations.Hastad.conditioned_coefficient_zero_invalid line 154
26. theorem OAI.IndependentSetsGames.Foundations.Hastad.conditioned_coefficient_support line 164
27. def OAI.IndependentSetsGames.Foundations.Hastad.conditionedFoldedAnswer line 174
28. theorem OAI.IndependentSetsGames.Foundations.Hastad.conditionedFoldedAnswer_flip line 179
29. theorem OAI.IndependentSetsGames.Foundations.Hastad.conditionedFoldedAnswer_zero_coefficient line 186
30. theorem OAI.IndependentSetsGames.Foundations.Hastad.conditionedFoldedAnswer_dictator line 193