OAI/Computability/BinPacking/Information/SourceHonest.lean

GitHub source file

161 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGames.Foundations.Hastad.dictator_test_parity line 21
2. theorem OAI.BinPackingGames.Foundations.Hastad.noise_coordinate_sign line 27
3. theorem OAI.BinPackingGames.Foundations.Hastad.noise_coordinate_false line 36
4. theorem OAI.BinPackingGames.Foundations.Hastad.testAcceptance_dictator line 49
5. theorem OAI.BinPackingGames.Foundations.Hastad.testAcceptance_folded_dictators line 67
6. theorem OAI.BinPackingGames.Foundations.Hastad.testAcceptance_conditioned_dictators line 78
7. theorem OAI.BinPackingGames.Foundations.Hastad.testAcceptance_folded_conditioned_dictators line 94
8. def OAI.BinPackingGames.Foundations.Hastad.realizedTestAcceptance line 107
9. theorem OAI.BinPackingGames.Foundations.Hastad.realizedTestAcceptance_eq_testAcceptance line 112
10. theorem OAI.BinPackingGames.Foundations.Hastad.realizedTestAcceptance_dictator line 121
11. theorem OAI.BinPackingGames.Foundations.Hastad.realizedTestAcceptance_folded_dictators line 127
12. theorem OAI.BinPackingGames.Foundations.Hastad.realizedTestAcceptance_conditioned_dictators line 134
13. theorem OAI.BinPackingGames.Foundations.Hastad.realizedTestAcceptance_folded_conditioned_dictators line 144
14. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceTape.TestTape line 159
15. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceTape.FairTestTape line 162
16. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.expect_prod line 168
17. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.card_testTape line 179
18. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.card_fairTestTape line 184
19. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.expect_testTape line 190
20. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.expect_equivTape line 198
21. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.expect_fairTestTape line 203
22. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.expect_fairTestTape_ignore line 212
23. def OAI.BinPackingGames.Foundations.Hastad.SourceTape.tapeQueries line 217
24. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.expect_tapeQueries line 220
25. def OAI.BinPackingGames.Foundations.Hastad.SourceTape.tapeAcceptance line 231
26. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_realizedTestAcceptance line 237
27. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_testAcceptance line 242
28. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_sum_div_card line 248
29. def OAI.BinPackingGames.Foundations.Hastad.SourceTape.restrictFunction line 260
30. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.expect_restrictFunction line 263
31. def OAI.BinPackingGames.Foundations.Hastad.SourceTape.restrictTape line 278
32. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.expect_restrictTape line 282
33. def OAI.BinPackingGames.Foundations.Hastad.SourceTape.restrictedProjection line 310
34. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.restrict_realizedNoise line 314
35. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.restrict_thirdQuery line 317
36. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.expect_restricted_queries line 323
37. def OAI.BinPackingGames.Foundations.Hastad.SourceTape.restrictRightTape line 335
38. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.expect_restrictRightTape line 339
39. theorem OAI.BinPackingGames.Foundations.Hastad.SourceTape.expect_rightRestricted_queries line 358
40. structure OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding line 377
41. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding.fin line 383
42. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding.bool line 384
43. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding.unit line 385
44. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding.prod line 387
45. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding.sum line 390
46. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding.function line 393
47. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate line 401
48. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding.length_enumerate line 403
49. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding.mem_enumerate line 406
50. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding.nodup_enumerate line 410
51. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.Encoding.card_eq_size line 413
52. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.GlobalKey line 419
53. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.globalEncoding line 421
54. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.globalEncoding_size line 427
55. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.extendRestricted line 432
56. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.extendRestricted_valid line 436
57. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.extendRestricted_injective line 440
58. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.restrictQuery_extendRestricted line 447
59. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.canonicalInput_half line 453
60. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey line 459
61. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_code line 464
62. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_surjective line 470
63. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.localAddress line 482
64. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.localAddress_injective line 489
65. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence line 514
66. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence_satisfied line 523
67. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.findValid line 552
68. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.findValid_none_iff line 556
69. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.firstValid line 565
70. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.firstValid_none_iff line 568
71. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.occurrenceList line 573
72. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.occurrenceList_length line 576
73. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.countP_cast_eq_sum line 580
74. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.countP_enumerate line 586
75. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.occurrenceList_acceptance line 593
76. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.clauseAnswerEncoding line 606
77. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.slotEncoding line 608
78. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.iEncoding line 616
79. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.jEncoding line 617
80. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.variableEncoding line 618
81. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.clauseEncoding line 620
82. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.slotContextEncoding line 622
83. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.proofEncoding line 625
84. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.nBits line 629
85. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.nBits_eq line 631
86. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.dummyIndex line 635
87. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.leftAnchor line 638
88. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.rightAnchor line 640
89. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.rightAnchor_none_iff line 643
90. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.halfTableKeyAssignment line 647
91. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.extendHalfTables line 659
92. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_left line 666
93. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_right line 677
94. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.emptyAddress line 694
95. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.contextEquation line 699
96. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.leftResponse line 708
97. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.rightResponse line 712
98. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.contextEquation_satisfied line 719
99. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.testTapeEncoding line 736
100. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.SourceIndex line 740
101. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.sourceIndexEncoding line 743
102. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.sourceEquation line 746
103. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.rawSourceList line 750
104. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.rawSourceList_length line 753
105. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.rawSourceList_acceptance line 760
106. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation line 783
107. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.sourceList line 786
108. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.sourceList_empty line 789
109. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.sourceList_nonempty line 792
110. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.sourceList_length_le_raw_add_one line 798
111. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.sourceList_ne_nil line 807
112. def OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.sourceInput line 818
113. theorem OAI.BinPackingGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation_satisfied line 822
114. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.event_nonempty line 834
115. def OAI.BinPackingGames.Foundations.Hastad.SourceGame.eventLaw line 838
116. def OAI.BinPackingGames.Foundations.Hastad.SourceGame.visibleQuestion line 843
117. def OAI.BinPackingGames.Foundations.Hastad.SourceGame.baseGame line 847
118. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.baseGame_accepts line 852
119. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.eventLaw_probability line 856
120. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.sum_slots line 869
121. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.sum_slot_accepts line 879
122. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.failureCount_eq_sum_map line 893
123. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.failureCount_allIndices line 901
124. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.verifier_probability_plus_failure line 908
125. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.base_success_le_verifier line 929
126. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.base_value_le_of_clause_gap line 939
127. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.pushforward_comp line 959
128. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.expectation_pushforward line 974
129. def OAI.BinPackingGames.Foundations.Hastad.SourceGame.repeatedVisible line 985
130. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.repeated_questions line 990
131. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.repeated_expectation line 999
132. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.repeated_expectation_split line 1010
133. def OAI.BinPackingGames.Foundations.Hastad.SourceGame.sourceProjectionGame line 1024
134. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.projection_value_le_repetition line 1029
135. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.source_acceptance_le line 1048
136. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGame.source_acceptance_le_split line 1063
137. def OAI.BinPackingGames.Foundations.Hastad.SourceHonest.taggedAssignment line 1088
138. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.taggedAssignment_left line 1094
139. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.taggedAssignment_right line 1098
140. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.taggedAssignment_right_restriction line 1102
141. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.conditioned_equation_honest_satisfied line 1118
142. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.mapped_conditioned_equation_honest_satisfied line 1129
143. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.tapeAcceptance_conditioned_dictators line 1150
144. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.numbered_assignment_restriction line 1168
145. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.conditionedOccurrence_honest_satisfied line 1186
146. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.conditionedOccurrenceList_honest_acceptance line 1201
147. def OAI.BinPackingGames.Foundations.Hastad.SourceHonest.honestGlobal line 1233
148. def OAI.BinPackingGames.Foundations.Hastad.SourceHonest.honestBits line 1239
149. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.honestBits_code line 1244
150. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.honestBits_dummy line 1252
151. def OAI.BinPackingGames.Foundations.Hastad.SourceHonest.honestValidJ line 1258
152. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.validJ_nonempty_of_satisfying line 1264
153. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.leftResponse_honest line 1270
154. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.rightResponse_honest line 1278
155. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.context_tapeAcceptance line 1301
156. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.sourceEquation_honest_satisfied line 1315
157. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.rawSourceList_honest_acceptance line 1325
158. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty line 1344
159. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance line 1354
160. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_rat line 1368
161. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty_rat line 1378