OAI/Computability/MinUncut/PCP/HonestTest.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MinUncutGames.Foundations.Hastad.dictator_test_parity line 18
2. theorem OAI.MinUncutGames.Foundations.Hastad.noise_coordinate_sign line 24
3. theorem OAI.MinUncutGames.Foundations.Hastad.noise_coordinate_false line 33
4. theorem OAI.MinUncutGames.Foundations.Hastad.testAcceptance_dictator line 46
5. theorem OAI.MinUncutGames.Foundations.Hastad.testAcceptance_folded_dictators line 64
6. theorem OAI.MinUncutGames.Foundations.Hastad.testAcceptance_conditioned_dictators line 75
7. theorem OAI.MinUncutGames.Foundations.Hastad.testAcceptance_folded_conditioned_dictators line 91
8. def OAI.MinUncutGames.Foundations.Hastad.realizedTestAcceptance line 104
9. theorem OAI.MinUncutGames.Foundations.Hastad.realizedTestAcceptance_eq_testAcceptance line 109
10. theorem OAI.MinUncutGames.Foundations.Hastad.realizedTestAcceptance_dictator line 118
11. theorem OAI.MinUncutGames.Foundations.Hastad.realizedTestAcceptance_folded_dictators line 124
12. theorem OAI.MinUncutGames.Foundations.Hastad.realizedTestAcceptance_conditioned_dictators line 131
13. theorem OAI.MinUncutGames.Foundations.Hastad.realizedTestAcceptance_folded_conditioned_dictators line 141
14. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceTape.TestTape line 156
15. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceTape.FairTestTape line 159
16. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.expect_prod line 165
17. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.card_testTape line 176
18. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.card_fairTestTape line 181
19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.expect_testTape line 187
20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.expect_equivTape line 195
21. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.expect_fairTestTape line 200
22. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.expect_fairTestTape_ignore line 209
23. def OAI.MinUncutGames.Foundations.Hastad.SourceTape.tapeQueries line 214
24. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.expect_tapeQueries line 217
25. def OAI.MinUncutGames.Foundations.Hastad.SourceTape.tapeAcceptance line 228
26. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_realizedTestAcceptance line 234
27. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_testAcceptance line 239
28. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_sum_div_card line 245
29. def OAI.MinUncutGames.Foundations.Hastad.SourceTape.restrictFunction line 257
30. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.expect_restrictFunction line 260
31. def OAI.MinUncutGames.Foundations.Hastad.SourceTape.restrictTape line 275
32. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.expect_restrictTape line 279
33. def OAI.MinUncutGames.Foundations.Hastad.SourceTape.restrictedProjection line 307
34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.restrict_realizedNoise line 311
35. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.restrict_thirdQuery line 314
36. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.expect_restricted_queries line 320
37. def OAI.MinUncutGames.Foundations.Hastad.SourceTape.restrictRightTape line 332
38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.expect_restrictRightTape line 336
39. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTape.expect_rightRestricted_queries line 355