OAI/Combinatorics/IndependentSets/Fourier/HonestTest.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.Hastad.dictator_test_parity line 18
  2. theorem OAI.IndependentSetsGames.Foundations.Hastad.noise_coordinate_sign line 24
  3. theorem OAI.IndependentSetsGames.Foundations.Hastad.noise_coordinate_false line 33
  4. theorem OAI.IndependentSetsGames.Foundations.Hastad.testAcceptance_dictator line 46
  5. theorem OAI.IndependentSetsGames.Foundations.Hastad.testAcceptance_folded_dictators line 64
  6. theorem OAI.IndependentSetsGames.Foundations.Hastad.testAcceptance_conditioned_dictators line 75
  7. theorem OAI.IndependentSetsGames.Foundations.Hastad.testAcceptance_folded_conditioned_dictators line 91
  8. def OAI.IndependentSetsGames.Foundations.Hastad.realizedTestAcceptance line 104
  9. theorem OAI.IndependentSetsGames.Foundations.Hastad.realizedTestAcceptance_eq_testAcceptance line 109
  10. theorem OAI.IndependentSetsGames.Foundations.Hastad.realizedTestAcceptance_dictator line 118
  11. theorem OAI.IndependentSetsGames.Foundations.Hastad.realizedTestAcceptance_folded_dictators line 124
  12. theorem OAI.IndependentSetsGames.Foundations.Hastad.realizedTestAcceptance_conditioned_dictators line 131
  13. theorem OAI.IndependentSetsGames.Foundations.Hastad.realizedTestAcceptance_folded_conditioned_dictators line 141