OAI/Computability/VertexCover/Fourier/FoldedEquation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.Hastad.FoldedEquation.Address line 46
  2. def OAI.UniqueGames.Foundations.Hastad.FoldedEquation.storedAssignment line 48
  3. def OAI.UniqueGames.Foundations.Hastad.FoldedEquation.rhsCorrection line 52
  4. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.correction_eq line 56
  5. def OAI.UniqueGames.Foundations.Hastad.FoldedEquation.equation line 63
  6. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.xor_corrections line 70
  7. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.equation_satisfied line 77
  8. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.equation_satisfied_iff line 89
  9. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.equation_indicator line 99
  10. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.satisfied_repeated_right line 110
  11. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.equation_repeated_right line 118
  12. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.restrict_thirdQuery line 128
  13. def OAI.UniqueGames.Foundations.Hastad.FoldedEquation.conditionedEquation line 134
  14. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.conditionedEquation_rhs line 140
  15. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied line 146
  16. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied_iff line 158
  17. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.conditionedEquation_indicator line 169
  18. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.conditionedEquation_repeated_right line 182
  19. def OAI.UniqueGames.Foundations.Hastad.FoldedEquation.equationAcceptance line 195
  20. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.equationAcceptance_eq line 201
  21. def OAI.UniqueGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance line 208
  22. theorem OAI.UniqueGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance_eq line 215