OAI/Computability/MinUncut/PCP/Walsh.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Hastad.Cube line 14
2. def OAI.MinUncutGames.Foundations.Hastad.bitSign line 16
3. theorem OAI.MinUncutGames.Foundations.Hastad.bitSign_sq line 18
4. theorem OAI.MinUncutGames.Foundations.Hastad.bitSign_xor line 21
5. def OAI.MinUncutGames.Foundations.Hastad.cubeXor line 25
6. def OAI.MinUncutGames.Foundations.Hastad.walsh line 27
7. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_symm line 30
8. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_sq line 34
9. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_xor line 38
10. theorem OAI.MinUncutGames.Foundations.Hastad.coordinate_orthogonality line 46
11. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_sum_orthogonality line 51
12. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_orthogonality line 68
13. def OAI.MinUncutGames.Foundations.Hastad.coefficient line 75
14. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_inversion line 78
15. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_inner line 95
16. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_parseval line 112
17. theorem OAI.MinUncutGames.Foundations.Hastad.sign_parseval line 116