OAI/Computability/VertexCover/Fourier/HonestTest.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGames.Foundations.Hastad.dictator_test_parity line 46
  2. theorem OAI.UniqueGames.Foundations.Hastad.noise_coordinate_sign line 52
  3. theorem OAI.UniqueGames.Foundations.Hastad.noise_coordinate_false line 61
  4. theorem OAI.UniqueGames.Foundations.Hastad.testAcceptance_dictator line 74
  5. theorem OAI.UniqueGames.Foundations.Hastad.testAcceptance_folded_dictators line 92
  6. theorem OAI.UniqueGames.Foundations.Hastad.testAcceptance_conditioned_dictators line 103
  7. theorem OAI.UniqueGames.Foundations.Hastad.testAcceptance_folded_conditioned_dictators line 119
  8. def OAI.UniqueGames.Foundations.Hastad.realizedTestAcceptance line 132
  9. theorem OAI.UniqueGames.Foundations.Hastad.realizedTestAcceptance_eq_testAcceptance line 137
  10. theorem OAI.UniqueGames.Foundations.Hastad.realizedTestAcceptance_dictator line 146
  11. theorem OAI.UniqueGames.Foundations.Hastad.realizedTestAcceptance_folded_dictators line 152
  12. theorem OAI.UniqueGames.Foundations.Hastad.realizedTestAcceptance_conditioned_dictators line 159
  13. theorem OAI.UniqueGames.Foundations.Hastad.realizedTestAcceptance_folded_conditioned_dictators line 169