OAI/Computability/DirectedFeedback/Games/ExpanderFamily.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.PCP.ExpanderFamily.Port line 11
  2. abbrev OAI.DFVSGames.Foundations.PCP.ExpanderFamily.CloudPort line 12
  3. def OAI.DFVSGames.Foundations.PCP.ExpanderFamily.growth line 13
  4. theorem OAI.DFVSGames.Foundations.PCP.ExpanderFamily.card_port line 15
  5. theorem OAI.DFVSGames.Foundations.PCP.ExpanderFamily.card_cloudPort line 19
  6. theorem OAI.DFVSGames.Foundations.PCP.ExpanderFamily.growth_gt_one line 25
  7. theorem OAI.DFVSGames.Foundations.PCP.ExpanderFamily.port_degree_ge_eight line 28
  8. def OAI.DFVSGames.Foundations.PCP.ExpanderFamily.baseVertexEquiv line 32
  9. def OAI.DFVSGames.Foundations.PCP.ExpanderFamily.baseOnCloud line 35
  10. theorem OAI.DFVSGames.Foundations.PCP.ExpanderFamily.baseOnCloud_certificate line 38
  11. def OAI.DFVSGames.Foundations.PCP.ExpanderFamily.Vertex line 41
  12. instance OAI.DFVSGames.Foundations.PCP.ExpanderFamily.vertexFintype line 45
  13. instance OAI.DFVSGames.Foundations.PCP.ExpanderFamily.basePortNonempty line 53
  14. instance OAI.DFVSGames.Foundations.PCP.ExpanderFamily.vertexNonempty line 56
  15. def OAI.DFVSGames.Foundations.PCP.ExpanderFamily.graph line 64
  16. theorem OAI.DFVSGames.Foundations.PCP.ExpanderFamily.graph_certificate line 68
  17. def OAI.DFVSGames.Foundations.PCP.ExpanderFamily.family line 91
  18. theorem OAI.DFVSGames.Foundations.PCP.ExpanderFamily.family_certificate line 93
  19. theorem OAI.DFVSGames.Foundations.PCP.ExpanderFamily.card_vertex line 96
  20. def OAI.DFVSGames.Foundations.PCP.ExpanderFamily.level line 103
  21. def OAI.DFVSGames.Foundations.PCP.ExpanderFamily.size line 105
  22. theorem OAI.DFVSGames.Foundations.PCP.ExpanderFamily.le_size line 107
  23. theorem OAI.DFVSGames.Foundations.PCP.ExpanderFamily.size_le_mul line 109
  24. theorem OAI.DFVSGames.Foundations.PCP.ExpanderFamily.padded_family_size line 123
  25. def OAI.DFVSGames.Foundations.PCP.CloudPadding.paddedSize line 139
  26. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.paddedSize_zero line 141
  27. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.paddedSize_of_pos line 143
  28. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.le_paddedSize line 147
  29. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.paddedSize_le_mul line 154
  30. def OAI.DFVSGames.Foundations.PCP.CloudPadding.paddedCloudEquiv line 161
  31. def OAI.DFVSGames.Foundations.PCP.CloudPadding.dartCloudEquiv line 184
  32. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.sum_card_cloud line 196
  33. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.card_padded_cloud line 200
  34. abbrev OAI.DFVSGames.Foundations.PCP.CloudPadding.dummy line 206
  35. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.card_cloud line 209
  36. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.card_dummy_of_empty line 217
  37. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.card_cloud_of_empty line 221
  38. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.card_cloud_eq_family line 226
  39. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.card_paddedDart_eq_sum line 234
  40. theorem OAI.DFVSGames.Foundations.PCP.CloudPadding.card_paddedDart_le line 246
  41. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv line 267
  42. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_val line 276
  43. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_symm_apply line 280
  44. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts line 284
  45. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.mem_cloudDarts line 287
  46. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_nodup line 291
  47. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_sublist line 295
  48. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize line 298
  49. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_le_darts line 300
  50. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect line 304
  51. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank line 309
  52. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_val line 314
  53. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_val line 318
  54. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_cloudRank line 322
  55. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_cloudSelect line 327
  56. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudEquiv line 332
  57. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_card_cloud line 339
  58. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_eq_nil_iff line 343
  59. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_zero_iff line 347
  60. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.sum_cloudSize line 351
  61. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.oldCloudIndex line 360
  62. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_oldCloudIndex line 363
  63. abbrev OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.PaddedCloud line 367
  64. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedOld line 371
  65. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedNew line 375
  66. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudEquiv line 379
  67. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank line 385
  68. def OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect line 389
  69. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_rank line 393
  70. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_select line 398
  71. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old line 403
  72. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new line 408
  73. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old_val line 413
  74. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new_val line 418
  75. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_castAdd line 423
  76. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_natAdd line 435
  77. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingCloudIndex.card_paddedCloud line 441
  78. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.rowIndex line 453
  79. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.rowIndex_val line 455
  80. structure OAI.DFVSGames.Foundations.PCP.ExpanderTables.Table line 458
  81. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.reverseIndex line 462
  82. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.lookup line 465
  83. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.lookup_involutive line 468
  84. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.graph line 475
  85. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.graph_rot line 479
  86. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.ofGraph line 482
  87. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.lookup_ofGraph line 490
  88. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.graph_ext_inline_ExpanderTables line 495
  89. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.graph_ofGraph line 503
  90. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.row_count line 506
  91. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.vertexIndex line 509
  92. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.stepGraph line 512
  93. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.step line 520
  94. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.stepLookup line 524
  95. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.lookup_step line 538
  96. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.step_certificate line 551
  97. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.initial line 562
  98. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.initial_certificate line 565
  99. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.vertexCount line 575
  100. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.vertexCount_eq line 579
  101. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.vertexCount_positive line 584
  102. def OAI.DFVSGames.Foundations.PCP.ExpanderTables.family line 589
  103. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.family_certificate line 594
  104. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.family_row_count line 605
  105. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTables.exists_base_table line 609
  106. def OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.levelLoop line 633
  107. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.levelLoop_level_le line 639
  108. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.levelLoop_power line 650
  109. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.levelLoop_covers line 661
  110. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.levelLoop_le_of_covering_power line 676
  111. def OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.searchResult line 693
  112. def OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.boundedLevel line 696
  113. def OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.paddedSize line 698
  114. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.boundedLevel_zero line 700
  115. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.paddedSize_zero line 702
  116. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_input line 704
  117. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.paddedSize_power line 708
  118. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.le_paddedSize line 713
  119. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.boundedLevel_eq_level line 717
  120. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.paddedSize_eq_size line 727
  121. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_of_le_power line 731
  122. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.paddedSize_positive line 736
  123. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.paddedSize_bounds line 740
  124. def OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize line 745
  125. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_zero line 747
  126. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_of_pos line 749
  127. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_bounds line 753
  128. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.table_vertexCount_eq_paddedSize line 761
  129. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingLevels.family_row_count_at_size line 772