OAI/Computability/MinUncut/PCP/ExpanderFamily.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.Port line 10
2. abbrev OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.CloudPort line 11
3. def OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.growth line 12
4. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.card_port line 14
5. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.card_cloudPort line 18
6. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.growth_gt_one line 24
7. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.port_degree_ge_eight line 27
8. def OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.baseVertexEquiv line 31
9. def OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.baseOnCloud line 34
10. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.baseOnCloud_certificate line 37
11. def OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.Vertex line 40
12. instance OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.vertexFintype line 44
13. instance OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.basePortNonempty line 52
14. instance OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.vertexNonempty line 55
15. def OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.graph line 63
16. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.graph_certificate line 67
17. def OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.family line 90
18. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.family_certificate line 92
19. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.card_vertex line 95
20. def OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.level line 102
21. def OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.size line 104
22. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.le_size line 106
23. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.size_le_mul line 108
24. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderFamily.padded_family_size line 122
25. def OAI.MinUncutGames.Foundations.PCP.CloudPadding.paddedSize line 137
26. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.paddedSize_zero line 139
27. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.paddedSize_of_pos line 141
28. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.le_paddedSize line 145
29. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.paddedSize_le_mul line 152
30. def OAI.MinUncutGames.Foundations.PCP.CloudPadding.paddedCloudEquiv line 159
31. def OAI.MinUncutGames.Foundations.PCP.CloudPadding.dartCloudEquiv line 182
32. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.sum_card_cloud line 193
33. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.card_padded_cloud line 197
34. abbrev OAI.MinUncutGames.Foundations.PCP.CloudPadding.dummy line 203
35. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.card_cloud line 206
36. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.card_dummy_of_empty line 214
37. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.card_cloud_of_empty line 218
38. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.card_cloud_eq_family line 223
39. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.card_paddedDart_eq_sum line 231
40. theorem OAI.MinUncutGames.Foundations.PCP.CloudPadding.card_paddedDart_le line 243
41. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv line 262
42. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_val line 271
43. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_symm_apply line 275
44. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts line 279
45. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.mem_cloudDarts line 282
46. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_nodup line 286
47. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_sublist line 290
48. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize line 293
49. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_le_darts line 295
50. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect line 299
51. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank line 304
52. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_val line 309
53. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_val line 313
54. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_cloudRank line 317
55. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_cloudSelect line 322
56. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudEquiv line 327
57. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_card_cloud line 334
58. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_eq_nil_iff line 338
59. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_zero_iff line 342
60. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.sum_cloudSize line 346
61. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.oldCloudIndex line 355
62. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_oldCloudIndex line 358
63. abbrev OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.PaddedCloud line 362
64. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedOld line 366
65. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedNew line 370
66. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudEquiv line 374
67. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank line 380
68. def OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect line 384
69. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_rank line 388
70. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_select line 393
71. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old line 398
72. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new line 403
73. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old_val line 408
74. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new_val line 413
75. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_castAdd line 418
76. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_natAdd line 430
77. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingCloudIndex.card_paddedCloud line 436
78. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.rowIndex line 447
79. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.rowIndex_val line 449
80. structure OAI.MinUncutGames.Foundations.PCP.ExpanderTables.Table line 452
81. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.reverseIndex line 456
82. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.lookup line 459
83. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.lookup_involutive line 462
84. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.graph line 469
85. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.graph_rot line 473
86. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.ofGraph line 476
87. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.lookup_ofGraph line 484
88. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.graph_ext line 489
89. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.graph_ofGraph line 497
90. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.row_count line 500
91. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.vertexIndex line 503
92. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.stepGraph line 506
93. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.step line 514
94. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.stepLookup line 518
95. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.lookup_step line 532
96. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.step_certificate line 544
97. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.initial line 555
98. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.initial_certificate line 558
99. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.vertexCount line 568
100. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.vertexCount_eq line 572
101. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.vertexCount_positive line 577
102. def OAI.MinUncutGames.Foundations.PCP.ExpanderTables.family line 582
103. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.family_certificate line 587
104. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.family_row_count line 598
105. theorem OAI.MinUncutGames.Foundations.PCP.ExpanderTables.exists_base_table line 602
106. def OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.levelLoop line 625
107. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.levelLoop_level_le line 631
108. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.levelLoop_power line 642
109. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.levelLoop_covers line 653
110. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.levelLoop_le_of_covering_power line 668
111. def OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.searchResult line 685
112. def OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.boundedLevel line 688
113. def OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.paddedSize line 690
114. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.boundedLevel_zero line 692
115. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.paddedSize_zero line 694
116. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_input line 696
117. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.paddedSize_power line 700
118. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.le_paddedSize line 705
119. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.boundedLevel_eq_level line 709
120. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.paddedSize_eq_size line 719
121. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_of_le_power line 723
122. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.paddedSize_positive line 728
123. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.paddedSize_bounds line 732
124. def OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize line 737
125. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_zero line 739
126. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_of_pos line 741
127. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_bounds line 745
128. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.table_vertexCount_eq_paddedSize line 753
129. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLevels.family_row_count_at_size line 764