OAI/Computability/BinPacking/Expanders/ExpanderTableEnumeration.lean

GitHub source file

186 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.upperMasks line 32
2. def OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.lowerMasks line 35
3. def OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.badMasks line 38
4. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.upperMasks_weight line 43
5. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.lowerMasks_complement_image line 60
6. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.lowerMasks_card_eq_upperMasks line 83
7. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.ratio_le_of_weight line 97
8. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.upperMasks_ratio_le line 111
9. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.lowerMasks_ratio_le line 116
10. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le_sharp line 121
11. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.badMasks_ratio_le line 136
12. def OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.trueMask line 146
13. def OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.countTrue line 149
14. def OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.badWord line 151
15. instance OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.(instance at line 154) line 154
16. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.bitSign_mean_eq line 157
17. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.not_badWord_bias line 173
18. def OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.wordMaskEquiv line 193
19. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.twoTail_probability line 203
20. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.union_bound_le_half line 224
21. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.fixed_parameters line 241
22. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.fixed_union_bound line 244
23. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.seventh_power_size line 248
24. theorem OAI.BinPackingGames.Foundations.PCP.CayleyTailCount.seventh_power_abs_le line 251
25. abbrev OAI.BinPackingGames.Foundations.PCP.CayleySampling.FalseFiber line 267
26. def OAI.BinPackingGames.Foundations.PCP.CayleySampling.falseRepresentative line 269
27. def OAI.BinPackingGames.Foundations.PCP.CayleySampling.booleanSplitEquiv line 274
28. theorem OAI.BinPackingGames.Foundations.PCP.CayleySampling.booleanSplitEquiv_fst line 290
29. def OAI.BinPackingGames.Foundations.PCP.CayleySampling.sampleSplitEquiv line 294
30. theorem OAI.BinPackingGames.Foundations.PCP.CayleySampling.sampleSplitEquiv_fst line 300
31. theorem OAI.BinPackingGames.Foundations.PCP.CayleySampling.card_boolean_split line 304
32. theorem OAI.BinPackingGames.Foundations.PCP.CayleySampling.expect_boolean_samples line 309
33. theorem OAI.BinPackingGames.Foundations.PCP.CayleySampling.exists_true_of_ne_zero line 329
34. theorem OAI.BinPackingGames.Foundations.PCP.CayleySampling.expect_parity_samples line 338
35. theorem OAI.BinPackingGames.Foundations.PCP.CayleySampling.expect_walsh_samples line 347
36. theorem OAI.BinPackingGames.Foundations.PCP.CayleySampling.expect_walsh_mean line 354
37. abbrev OAI.BinPackingGames.Foundations.PCP.Expanders.Generators line 367
38. def OAI.BinPackingGames.Foundations.PCP.Expanders.badFrequency line 369
39. def OAI.BinPackingGames.Foundations.PCP.Expanders.badMass line 373
40. theorem OAI.BinPackingGames.Foundations.PCP.Expanders.badFrequency_nonnegative line 376
41. theorem OAI.BinPackingGames.Foundations.PCP.Expanders.mean_badFrequency_le line 381
42. theorem OAI.BinPackingGames.Foundations.PCP.Expanders.mean_badMass_le line 393
43. theorem OAI.BinPackingGames.Foundations.PCP.Expanders.exists_generators line 405
44. def OAI.BinPackingGames.Foundations.PCP.Expanders.baseDimension line 426
45. def OAI.BinPackingGames.Foundations.PCP.Expanders.initialDegree line 427
46. def OAI.BinPackingGames.Foundations.PCP.Expanders.initialQuarterDegree line 428
47. def OAI.BinPackingGames.Foundations.PCP.Expanders.basePower line 429
48. theorem OAI.BinPackingGames.Foundations.PCP.Expanders.base_arithmetic line 431
49. theorem OAI.BinPackingGames.Foundations.PCP.Expanders.exists_initial_generators line 443
50. abbrev OAI.BinPackingGames.Foundations.PCP.Expanders.BaseVertex line 449
51. abbrev OAI.BinPackingGames.Foundations.PCP.Expanders.BasePort line 450
52. def OAI.BinPackingGames.Foundations.PCP.Expanders.baseDegree line 451
53. theorem OAI.BinPackingGames.Foundations.PCP.Expanders.card_basePort line 453
54. theorem OAI.BinPackingGames.Foundations.PCP.Expanders.card_baseVertex line 458
55. theorem OAI.BinPackingGames.Foundations.PCP.Expanders.exists_baseGraph line 462
56. abbrev OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.Port line 480
57. abbrev OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.CloudPort line 481
58. def OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.growth line 482
59. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.card_port line 484
60. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.card_cloudPort line 488
61. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.growth_gt_one line 494
62. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.port_degree_ge_eight line 497
63. def OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.baseVertexEquiv line 501
64. def OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.baseOnCloud line 504
65. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.baseOnCloud_certificate line 507
66. def OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.Vertex line 510
67. instance OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.vertexFintype line 514
68. instance OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.basePortNonempty line 522
69. instance OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.vertexNonempty line 525
70. def OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.graph line 533
71. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.graph_certificate line 537
72. def OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.family line 560
73. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.family_certificate line 562
74. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.card_vertex line 565
75. def OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.level line 572
76. def OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.size line 574
77. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.le_size line 576
78. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.size_le_mul line 578
79. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderFamily.padded_family_size line 592
80. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.rowIndex line 604
81. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.rowIndex_val line 606
82. structure OAI.BinPackingGames.Foundations.PCP.ExpanderTables.Table line 609
83. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.reverseIndex line 613
84. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.lookup line 616
85. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.lookup_involutive line 619
86. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.graph line 626
87. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.graph_rot line 630
88. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.ofGraph line 633
89. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.lookup_ofGraph line 641
90. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.graph_ext line 646
91. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.graph_ofGraph line 654
92. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.row_count line 657
93. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.vertexIndex line 660
94. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.stepGraph line 663
95. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.step line 671
96. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.stepLookup line 675
97. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.lookup_step line 689
98. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.step_certificate line 701
99. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.initial line 712
100. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.initial_certificate line 715
101. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.vertexCount line 725
102. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.vertexCount_eq line 729
103. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.vertexCount_positive line 734
104. def OAI.BinPackingGames.Foundations.PCP.ExpanderTables.family line 739
105. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.family_certificate line 744
106. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.family_row_count line 755
107. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTables.exists_base_table line 759
108. abbrev OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.degree line 784
109. abbrev OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.cloudSize line 785
110. abbrev OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.rowFactor line 786
111. structure OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.Control line 788
112. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.squarePorts line 796
113. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.start line 799
114. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.receiveFirst line 810
115. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.receiveSecond line 813
116. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.firstOffset line 820
117. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.secondOffset line 821
118. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.outputPort line 823
119. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.outputOffset line 826
120. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.firstAddress line 829
121. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.secondAddress line 832
122. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.outputAddress line 835
123. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.firstOffset_receiveFirst line 838
124. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.secondOffset_receiveFirst line 841
125. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.receiveFirst_port line 844
126. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.receiveSecond_port line 847
127. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.firstAddress_eq_rowIndex line 850
128. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.secondAddress_eq_rowIndex line 856
129. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.firstAddress_lt line 862
130. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.secondAddress_lt line 867
131. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.lookup_vertex_div line 872
132. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.lookup_port_mod line 875
133. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.lookup_port_eq_remainder line 878
134. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.rowIndex_lookup line 882
135. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.outputPair line 886
136. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_rowIndex line 890
137. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.outputAddress_lt line 896
138. def OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.evaluateRow line 901
139. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.evaluateRow_eq_lookup_step line 910
140. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_row line 919
141. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderRowControl.outputAddress_eq_step_reverseIndex line 927
142. def OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.rotationWords line 944
143. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.rotationWords_length line 946
144. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem line 950
145. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.rotationWords_get line 956
146. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem? line 962
147. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem?_none line 968
148. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.rotationWords_entry_lt line 972
149. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.rotationWords_lookup line 977
150. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.rotationWords_row_order line 983
151. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.decode_rotationWords line 988
152. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.decoded_lookup line 992
153. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.decoded_coordinate_lookup line 998
154. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_eq line 1005
155. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_le line 1009
156. def OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.globalIndex line 1026
157. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.globalIndex_val line 1032
158. def OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.rowValue line 1045
159. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.rowValue_eq_reverseIndex line 1051
160. def OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords line 1058
161. def OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords line 1061
162. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_length line 1064
163. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_succ line 1068
164. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_full line 1075
165. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_last line 1080
166. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.ofFn_cast line 1086
167. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.rotationWords_eq_ofFn line 1091
168. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.rowCount_eq line 1099
169. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_eq_flat_ofFn line 1102
170. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_eq_rotationWords line 1120
171. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_length line 1127
172. def OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices line 1132
173. def OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows line 1135
174. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_zero line 1139
175. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_full line 1142
176. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_succ line 1147
177. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_zero line 1154
178. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_succ line 1158
179. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_complete line 1166
180. def OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.accumulate line 1172
181. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_eq line 1175
182. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_append line 1183
183. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_prefixRows_succ line 1187
184. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_generatedWords line 1195
185. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.encode_generatedWords_length_le line 1201
186. theorem OAI.BinPackingGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_generatedWords_length_le line 1207