OAI/Combinatorics/IndependentSets/Fourier/FoldedEquation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.Address line 14
2. def OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.storedAssignment line 16
3. def OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.rhsCorrection line 20
4. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.correction_eq line 23
5. def OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.equation line 30
6. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.xor_corrections line 37
7. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.equation_satisfied line 42
8. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.equation_satisfied_iff line 53
9. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.equation_indicator line 62
10. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.satisfied_repeated_right line 73
11. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.equation_repeated_right line 80
12. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.restrict_thirdQuery line 89
13. def OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.conditionedEquation line 95
14. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.conditionedEquation_rhs line 100
15. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied line 105
16. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied_iff line 116
17. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.conditionedEquation_indicator line 126
18. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.conditionedEquation_repeated_right line 138
19. def OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.equationAcceptance line 153
20. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.equationAcceptance_eq line 159
21. def OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance line 166
22. theorem OAI.IndependentSetsGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance_eq line 173