OAI/Computability/VertexCover/Fourier/EmptyContext.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.Hastad.mapEquation line 43
  2. theorem OAI.UniqueGames.Foundations.Hastad.satisfied_mapEquation line 50
  3. abbrev OAI.UniqueGames.Foundations.Hastad.EmptyContext.Address line 58
  4. def OAI.UniqueGames.Foundations.Hastad.EmptyContext.storedAssignment line 60
  5. def OAI.UniqueGames.Foundations.Hastad.EmptyContext.equation line 63
  6. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.equation_second_eq_third line 70
  7. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.equation_satisfied line 75
  8. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.equation_storedAssignment_satisfied line 84
  9. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.equation_flip_first line 91
  10. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.equation_flip_rhs line 97
  11. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.equation_satisfied_flip line 101
  12. def OAI.UniqueGames.Foundations.Hastad.EmptyContext.pairedEquations line 107
  13. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.pairedEquations_length line 111
  14. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.pairedEquations_ne_nil line 115
  15. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.pairedEquations_acceptedCount line 120
  16. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.pairedEquations_failureCount line 127
  17. def OAI.UniqueGames.Foundations.Hastad.EmptyContext.equationAcceptance line 135
  18. def OAI.UniqueGames.Foundations.Hastad.EmptyContext.equationBias line 138
  19. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.foldedMean_eq_zero line 141
  20. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.equation_indicator line 146
  21. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.equationAcceptance_eq_half line 152
  22. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.equationBias_eq_zero line 159
  23. theorem OAI.UniqueGames.Foundations.Hastad.EmptyContext.mapped_equationAcceptance_eq_half line 170