OAI/Computability/VertexCover/Fourier/SourceTape.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.Hastad.SourceTape.TestTape line 42
  2. abbrev OAI.UniqueGames.Foundations.Hastad.SourceTape.FairTestTape line 45
  3. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.expect_prod line 51
  4. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.card_testTape line 62
  5. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.card_fairTestTape line 67
  6. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.expect_testTape line 73
  7. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.expect_equivTape line 81
  8. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.expect_fairTestTape line 86
  9. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.expect_fairTestTape_ignore line 95
  10. def OAI.UniqueGames.Foundations.Hastad.SourceTape.tapeQueries line 100
  11. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.expect_tapeQueries line 103
  12. def OAI.UniqueGames.Foundations.Hastad.SourceTape.tapeAcceptance line 114
  13. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_realizedTestAcceptance line 120
  14. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_testAcceptance line 125
  15. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_sum_div_card line 131
  16. def OAI.UniqueGames.Foundations.Hastad.SourceTape.restrictFunction line 145
  17. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.expect_restrictFunction line 148
  18. def OAI.UniqueGames.Foundations.Hastad.SourceTape.restrictTape line 163
  19. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.expect_restrictTape line 167
  20. def OAI.UniqueGames.Foundations.Hastad.SourceTape.restrictedProjection line 195
  21. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.restrict_realizedNoise line 199
  22. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.restrict_thirdQuery line 202
  23. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.expect_restricted_queries line 208
  24. def OAI.UniqueGames.Foundations.Hastad.SourceTape.restrictRightTape line 220
  25. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.expect_restrictRightTape line 224
  26. theorem OAI.UniqueGames.Foundations.Hastad.SourceTape.expect_rightRestricted_queries line 243