OAI/Computability/BinPacking/PCP/FinalConstants.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.PCP.VertexPadding.reverseFunction line 19
  2. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.reverseFunction_involutive line 24
  3. def OAI.BinPackingGames.Foundations.PCP.VertexPadding.pad line 32
  4. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.pad_tail line 50
  5. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.pad_reverse_inl line 53
  6. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.pad_reverse_inr line 58
  7. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.edgeSatisfied_inl line 62
  8. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.edgeSatisfied_inr line 73
  9. def OAI.BinPackingGames.Foundations.PCP.VertexPadding.extendLabeling line 77
  10. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.extendLabeling_inl line 80
  11. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.extendLabeling_inr line 83
  12. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.pad_satisfiable line 86
  13. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.satisfiable_of_pad line 94
  14. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.rejectionCount_eq_sum line 101
  15. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.pad_rejectionCount line 106
  16. def OAI.BinPackingGames.Foundations.PCP.VertexPadding.extraVertices line 118
  17. abbrev OAI.BinPackingGames.Foundations.PCP.VertexPadding.Vertex line 120
  18. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.card_vertex line 122
  19. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.le_card_vertex line 126
  20. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.card_vertex_le line 130
  21. def OAI.BinPackingGames.Foundations.PCP.VertexPadding.familyVertexEquiv line 135
  22. def OAI.BinPackingGames.Foundations.PCP.VertexPadding.paddedG line 143
  23. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.paddedG_tail line 146
  24. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.paddedG_rejectionCount line 149
  25. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.rejectionCount_eq line 156
  26. def OAI.BinPackingGames.Foundations.PCP.VertexPadding.liftLabel line 163
  27. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.liftLabel_inl line 166
  28. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.liftLabel_inr line 169
  29. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.rejectionCount_liftLabel line 173
  30. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.paddedG_satisfiable line 180
  31. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.card_padded_darts line 184
  32. theorem OAI.BinPackingGames.Foundations.PCP.VertexPadding.card_padded_darts_le line 188
  33. def OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv line 201
  34. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inl line 204
  35. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inr_val line 207
  36. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_symm_old line 210
  37. def OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv line 214
  38. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv_apply line 218
  39. def OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.sumGraph line 222
  40. def OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph line 227
  41. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_reverse_equiv line 244
  42. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_accepts_equiv line 252
  43. def OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.pad line 259
  44. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad line 265
  45. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad line 269
  46. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.pad_valid line 274
  47. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.constraintGraph_ext line 280
  48. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.baseGraph_pad line 294
  49. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_equiv line 302
  50. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_old line 310
  51. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_new line 317
  52. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_old line 324
  53. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_new line 331
  54. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_old line 337
  55. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_new line 343
  56. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.relation_ext line 349
  57. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_old line 358
  58. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_new line 366
  59. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_edgeSatisfied_equiv line 376
  60. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_equiv line 389
  61. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_old line 396
  62. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_new line 404
  63. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.pad_rejectionCount line 410
  64. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.pad_labeling_satisfies_iff line 428
  65. def OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling line 443
  66. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling_old line 446
  67. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingTables.pad_satisfiable_iff line 450
  68. abbrev OAI.BinPackingGames.Foundations.PCP.Preprocessing.Vertex line 470
  69. abbrev OAI.BinPackingGames.Foundations.PCP.Preprocessing.OverlayPort line 471
  70. abbrev OAI.BinPackingGames.Foundations.PCP.Preprocessing.Port line 472
  71. def OAI.BinPackingGames.Foundations.PCP.Preprocessing.degree line 474
  72. def OAI.BinPackingGames.Foundations.PCP.Preprocessing.sizeFactor line 475
  73. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.card_lazy_sum line 477
  74. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.doubled_add line 482
  75. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.degree_eq_card line 484
  76. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.degree_positive line 493
  77. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.sizeFactor_positive line 497
  78. def OAI.BinPackingGames.Foundations.PCP.Preprocessing.paddedGraph line 502
  79. def OAI.BinPackingGames.Foundations.PCP.Preprocessing.overlayExpander line 506
  80. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.overlayExpander_certificate line 513
  81. def OAI.BinPackingGames.Foundations.PCP.Preprocessing.overlayGraph line 517
  82. def OAI.BinPackingGames.Foundations.PCP.Preprocessing.graph line 521
  83. def OAI.BinPackingGames.Foundations.PCP.Preprocessing.portGraph line 525
  84. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.graph_tail line 529
  85. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.graph_reverse line 532
  86. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.accepts_reverse line 536
  87. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.portGraph_eq_lazyGraph line 541
  88. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.overlayGraph_certificate line 545
  89. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.spectral_certificate line 554
  90. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.vertex_count_le line 560
  91. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.dart_count line 570
  92. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.dart_count_le line 575
  93. def OAI.BinPackingGames.Foundations.PCP.Preprocessing.liftLabel line 583
  94. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.lift_rejectionCount line 587
  95. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.completeness line 598
  96. def OAI.BinPackingGames.Foundations.PCP.Preprocessing.roundLabels line 605
  97. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.soundness line 609
  98. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.satisfiable_iff line 622
  99. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.gap_transfer line 634
  100. theorem OAI.BinPackingGames.Foundations.PCP.Preprocessing.gap_transfer_real line 650
  101. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.encodeWords_flatMap line 676
  102. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.ofFn_split line 682
  103. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.flatten_ofFn_rowIndex line 692
  104. def OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.rowBits line 707
  105. def OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits line 711
  106. def OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits line 714
  107. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_flat line 717
  108. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits_eq_vertices line 723
  109. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_old line 737
  110. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_new line 749
  111. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.dummy_rowsBits_eq_ofFn line 759
  112. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.paddingBits_eq_ofFn line 773
  113. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_old line 787
  114. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_new line 791
  115. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits_pad line 803
  116. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingWords.tableBits_pad line 810
  117. def OAI.BinPackingGames.Foundations.PCP.FinalConstants.alphabet line 823
  118. def OAI.BinPackingGames.Foundations.PCP.FinalConstants.compositionLoss line 824
  119. def OAI.BinPackingGames.Foundations.PCP.FinalConstants.denominator line 825
  120. def OAI.BinPackingGames.Foundations.PCP.FinalConstants.windowHalf line 826
  121. def OAI.BinPackingGames.Foundations.PCP.FinalConstants.windowSize line 827
  122. def OAI.BinPackingGames.Foundations.PCP.FinalConstants.smoothingScale line 828
  123. def OAI.BinPackingGames.Foundations.PCP.FinalConstants.endpointLength line 829
  124. def OAI.BinPackingGames.Foundations.PCP.FinalConstants.walkLength line 830
  125. def OAI.BinPackingGames.Foundations.PCP.FinalConstants.gain line 832
  126. def OAI.BinPackingGames.Foundations.PCP.FinalConstants.cap line 833
  127. theorem OAI.BinPackingGames.Foundations.PCP.FinalConstants.denominator_positive line 835
  128. theorem OAI.BinPackingGames.Foundations.PCP.FinalConstants.windowHalf_positive line 838
  129. theorem OAI.BinPackingGames.Foundations.PCP.FinalConstants.walkLength_positive line 841
  130. theorem OAI.BinPackingGames.Foundations.PCP.FinalConstants.gain_large line 844
  131. theorem OAI.BinPackingGames.Foundations.PCP.FinalConstants.cap_positive line 851
  132. theorem OAI.BinPackingGames.Foundations.PCP.FinalConstants.cap_le_one line 854
  133. theorem OAI.BinPackingGames.Foundations.PCP.FinalConstants.composed_gap line 858