OAI/Computability/VertexCover/Fourier/Folding.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.Hastad.cubeFlip line 17
  2. theorem OAI.UniqueGames.Foundations.Hastad.cubeFlip_cubeFlip line 20
  3. theorem OAI.UniqueGames.Foundations.Hastad.bitSign_not line 24
  4. theorem OAI.UniqueGames.Foundations.Hastad.sum_cubeFlip line 27
  5. theorem OAI.UniqueGames.Foundations.Hastad.coefficient_zero_of_odd line 39
  6. theorem OAI.UniqueGames.Foundations.Hastad.coefficient_sign_zero_of_folded line 48
  7. def OAI.UniqueGames.Foundations.Hastad.representative line 55
  8. theorem OAI.UniqueGames.Foundations.Hastad.representative_at line 59
  9. theorem OAI.UniqueGames.Foundations.Hastad.representative_flip line 64
  10. abbrev OAI.UniqueGames.Foundations.Hastad.HalfCube line 68
  11. def OAI.UniqueGames.Foundations.Hastad.canonicalInput line 70
  12. theorem OAI.UniqueGames.Foundations.Hastad.canonicalInput_flip line 74
  13. def OAI.UniqueGames.Foundations.Hastad.foldedAnswer line 79
  14. theorem OAI.UniqueGames.Foundations.Hastad.foldedAnswer_flip line 83
  15. theorem OAI.UniqueGames.Foundations.Hastad.foldedAnswer_zero_coefficient line 91
  16. theorem OAI.UniqueGames.Foundations.Hastad.foldedAnswer_dictator line 96
  17. def OAI.UniqueGames.Foundations.Hastad.coordinateMask line 101
  18. def OAI.UniqueGames.Foundations.Hastad.cubeToggle line 103
  19. theorem OAI.UniqueGames.Foundations.Hastad.cubeToggle_twice line 107
  20. theorem OAI.UniqueGames.Foundations.Hastad.walsh_coordinateMask line 113
  21. theorem OAI.UniqueGames.Foundations.Hastad.walsh_cubeToggle line 123
  22. theorem OAI.UniqueGames.Foundations.Hastad.sum_cubeToggle line 128
  23. def OAI.UniqueGames.Foundations.Hastad.restrictQuery line 141
  24. theorem OAI.UniqueGames.Foundations.Hastad.restrictQuery_cubeToggle line 145
  25. theorem OAI.UniqueGames.Foundations.Hastad.conditioned_coefficient_zero_invalid line 156
  26. theorem OAI.UniqueGames.Foundations.Hastad.conditioned_coefficient_support line 166
  27. def OAI.UniqueGames.Foundations.Hastad.conditionedFoldedAnswer line 176
  28. theorem OAI.UniqueGames.Foundations.Hastad.conditionedFoldedAnswer_flip line 181
  29. theorem OAI.UniqueGames.Foundations.Hastad.conditionedFoldedAnswer_zero_coefficient line 188
  30. theorem OAI.UniqueGames.Foundations.Hastad.conditionedFoldedAnswer_dictator line 195