OAI/Computability/MinUncut/PCP/Game.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.event_nonempty line 14
2. def OAI.MinUncutGames.Foundations.Hastad.SourceGame.eventLaw line 18
3. def OAI.MinUncutGames.Foundations.Hastad.SourceGame.visibleQuestion line 23
4. def OAI.MinUncutGames.Foundations.Hastad.SourceGame.baseGame line 27
5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.baseGame_accepts line 32
6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.eventLaw_probability line 36
7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.sum_slots line 49
8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.sum_slot_accepts line 59
9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.failureCount_eq_sum_map line 73
10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.failureCount_allIndices line 81
11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.verifier_probability_plus_failure line 88
12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.base_success_le_verifier line 109
13. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.base_value_le_of_clause_gap line 119
14. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.pushforward_comp line 139
15. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.expectation_pushforward line 154
16. def OAI.MinUncutGames.Foundations.Hastad.SourceGame.repeatedVisible line 165
17. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.repeated_questions line 170
18. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.repeated_expectation line 179
19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.repeated_expectation_split line 190
20. def OAI.MinUncutGames.Foundations.Hastad.SourceGame.sourceProjectionGame line 204
21. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.projection_value_le_repetition line 209
22. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.source_acceptance_le line 228
23. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGame.source_acceptance_le_split line 243
24. def OAI.MinUncutGames.Foundations.Hastad.SourceSoundness.leftTable line 267
25. def OAI.MinUncutGames.Foundations.Hastad.SourceSoundness.rightOracle line 271
26. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSoundness.rightOracle_answer line 279
27. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSoundness.leftTable_answer line 285
28. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSoundness.sourceList_sound line 289
29. theorem OAI.MinUncutGames.Foundations.Hastad.SourceSoundness.sourceList_sound_rat line 307
30. def OAI.MinUncutGames.Foundations.Hastad.SourceHonest.taggedAssignment line 329
31. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.taggedAssignment_left line 335
32. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.taggedAssignment_right line 339
33. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.taggedAssignment_right_restriction line 343
34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.conditioned_equation_honest_satisfied line 360
35. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.mapped_conditioned_equation_honest_satisfied line 372
36. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.tapeAcceptance_conditioned_dictators line 391
37. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.numbered_assignment_restriction line 409
38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.conditionedOccurrence_honest_satisfied line 430
39. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.conditionedOccurrenceList_honest_acceptance line 443
40. def OAI.MinUncutGames.Foundations.Hastad.SourceHonest.honestGlobal line 476
41. def OAI.MinUncutGames.Foundations.Hastad.SourceHonest.honestBits line 482
42. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.honestBits_code line 487
43. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.honestBits_dummy line 495
44. def OAI.MinUncutGames.Foundations.Hastad.SourceHonest.honestValidJ line 501
45. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.validJ_nonempty_of_satisfying line 507
46. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.leftResponse_honest line 513
47. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.rightResponse_honest line 521
48. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.context_tapeAcceptance line 544
49. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.sourceEquation_honest_satisfied line 558
50. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.rawSourceList_honest_acceptance line 568
51. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty line 587
52. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance line 597
53. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_rat line 611
54. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty_rat line 621
55. def OAI.MinUncutGames.Soundness.RepetitionUpper.bernoulliAverage line 637
56. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.bernoulliAverage_scale line 643
57. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.bernoulliAverage_geometric line 651
58. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.bernoulliAverage_mono line 663
59. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.success_le_geometric line 678
60. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.pow_mono_nonneg line 689
61. def OAI.MinUncutGames.Soundness.RepetitionUpper.zeroProbability line 701
62. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.zeroProbability_nonneg line 703
63. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.zeroProbability_le_one line 706
64. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.zeroProbability_antitone line 714
65. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.geometric_le_dimension_bound line 733
66. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.projection_upper_bound line 747
67. def OAI.MinUncutGames.Soundness.RepetitionUpper.decoderThreshold line 758
68. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.decoderThreshold_pos line 760
69. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.exists_pos_nat_gt line 769
70. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.power_mul_growth_le_one line 778
71. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.exists_power_lt line 796
72. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.zeroProbability_pos line 813
73. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.exists_repetition_length line 816
74. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.soundness_of_bounds line 830
75. theorem OAI.MinUncutGames.Soundness.RepetitionUpper.soundness_from_repetition line 845