OAI/Combinatorics/IndependentSets/Fourier/Walsh.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Hastad.Cube line 12
  2. def OAI.IndependentSetsGames.Foundations.Hastad.bitSign line 14
  3. theorem OAI.IndependentSetsGames.Foundations.Hastad.bitSign_sq line 16
  4. theorem OAI.IndependentSetsGames.Foundations.Hastad.bitSign_xor line 19
  5. def OAI.IndependentSetsGames.Foundations.Hastad.cubeXor line 23
  6. def OAI.IndependentSetsGames.Foundations.Hastad.walsh line 25
  7. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_symm line 28
  8. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_sq line 32
  9. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_xor line 36
  10. theorem OAI.IndependentSetsGames.Foundations.Hastad.coordinate_orthogonality line 44
  11. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_sum_orthogonality line 49
  12. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_orthogonality line 66
  13. def OAI.IndependentSetsGames.Foundations.Hastad.coefficient line 73
  14. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_inversion line 76
  15. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_inner line 93
  16. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_parseval line 110
  17. theorem OAI.IndependentSetsGames.Foundations.Hastad.sign_parseval line 114
  18. def OAI.IndependentSetsGames.Foundations.Hastad.support line 121
  19. def OAI.IndependentSetsGames.Foundations.Hastad.noiseWeight line 123
  20. theorem OAI.IndependentSetsGames.Foundations.Hastad.noiseWeight_nonneg line 127
  21. theorem OAI.IndependentSetsGames.Foundations.Hastad.noiseWeight_sum line 133
  22. theorem OAI.IndependentSetsGames.Foundations.Hastad.noise_walsh line 138
  23. def OAI.IndependentSetsGames.Foundations.Hastad.thirdQuery line 152
  24. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_autocorrelation line 155
  25. def OAI.IndependentSetsGames.Foundations.Hastad.projectedCoefficient line 173
  26. def OAI.IndependentSetsGames.Foundations.Hastad.testBias line 176
  27. theorem OAI.IndependentSetsGames.Foundations.Hastad.testBias_fourier line 180
  28. def OAI.IndependentSetsGames.Foundations.Hastad.testAcceptance line 208
  29. theorem OAI.IndependentSetsGames.Foundations.Hastad.threeBit_indicator line 213
  30. theorem OAI.IndependentSetsGames.Foundations.Hastad.testAcceptance_eq line 218