OAI/Computability/BinPacking/PCP/PCPIteration.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.AmplificationIteration.run line 14
2. theorem OAI.BinPackingGames.Foundations.PCP.AmplificationIteration.min_double_min line 18
3. theorem OAI.BinPackingGames.Foundations.PCP.AmplificationIteration.run_gap line 26
4. theorem OAI.BinPackingGames.Foundations.PCP.AmplificationIteration.run_preserves line 41
5. theorem OAI.BinPackingGames.Foundations.PCP.AmplificationIteration.run_size line 48
6. def OAI.BinPackingGames.Foundations.PCP.AmplificationIteration.rounds line 57
7. theorem OAI.BinPackingGames.Foundations.PCP.AmplificationIteration.rounds_large line 59
8. theorem OAI.BinPackingGames.Foundations.PCP.AmplificationIteration.rounds_power_le line 63
9. theorem OAI.BinPackingGames.Foundations.PCP.AmplificationIteration.blowup_rounds_le line 68
10. theorem OAI.BinPackingGames.Foundations.PCP.AmplificationIteration.run_size_polynomial line 76
11. theorem OAI.BinPackingGames.Foundations.PCP.AmplificationIteration.run_reaches_cap line 83
12. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.OutputVertex line 101
13. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.OutputDart line 104
14. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.localEventFactor line 106
15. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.vertexFactor line 109
16. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.dartFactor line 111
17. def OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor line 113
18. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor_positive line 115
19. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.gap_transfer_real line 122
20. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex line 161
21. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart line 170
22. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.card_output_total line 176
23. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.card_output_total_le line 183
24. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex_le line 200
25. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart_le line 205
26. abbrev OAI.BinPackingGames.Foundations.PCP.AmplificationRound.Label line 214
27. abbrev OAI.BinPackingGames.Foundations.PCP.AmplificationRound.Addresses line 215
28. abbrev OAI.BinPackingGames.Foundations.PCP.AmplificationRound.PoweredAlphabet line 216
29. instance OAI.BinPackingGames.Foundations.PCP.AmplificationRound.(instance at line 219) line 219
30. instance OAI.BinPackingGames.Foundations.PCP.AmplificationRound.(instance at line 220) line 220
31. abbrev OAI.BinPackingGames.Foundations.PCP.AmplificationRound.PoweredDart line 225
32. instance OAI.BinPackingGames.Foundations.PCP.AmplificationRound.(instance at line 229) line 229
33. def OAI.BinPackingGames.Foundations.PCP.AmplificationRound.selectors line 231
34. def OAI.BinPackingGames.Foundations.PCP.AmplificationRound.powered line 238
35. abbrev OAI.BinPackingGames.Foundations.PCP.AmplificationRound.Vertex line 244
36. abbrev OAI.BinPackingGames.Foundations.PCP.AmplificationRound.Dart line 249
37. instance OAI.BinPackingGames.Foundations.PCP.AmplificationRound.(instance at line 252) line 252
38. instance OAI.BinPackingGames.Foundations.PCP.AmplificationRound.(instance at line 261) line 261
39. instance OAI.BinPackingGames.Foundations.PCP.AmplificationRound.(instance at line 264) line 264
40. def OAI.BinPackingGames.Foundations.PCP.AmplificationRound.graph line 266
41. theorem OAI.BinPackingGames.Foundations.PCP.AmplificationRound.powered_completeness line 271
42. theorem OAI.BinPackingGames.Foundations.PCP.AmplificationRound.completeness line 284
43. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.card_padded_alphabet line 296
44. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.card_powered_dart line 303
45. opaque OAI.BinPackingGames.Foundations.PCP.RoundSize.lockedNat line 310
46. def OAI.BinPackingGames.Foundations.PCP.RoundSize.poweredAlphabetSize line 312
47. def OAI.BinPackingGames.Foundations.PCP.RoundSize.poweredDartFactor line 316
48. def OAI.BinPackingGames.Foundations.PCP.RoundSize.sizeFactor line 319
49. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.poweredAlphabetSize_eq line 323
50. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.poweredDartFactor_eq line 327
51. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.sizeFactor_eq line 331
52. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.coefficient_positive line 335
53. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.poweredAlphabet_card line 340
54. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.sizeFactor_positive line 349
55. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.factor_total line 355
56. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.nat_card_output_vertex line 358
57. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.nat_card_output_dart line 366
58. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.nat_card_output_total_le line 373
59. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.poweredDart_card line 385
60. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.output_vertex_card line 396
61. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.output_dart_card line 411
62. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.output_total_le_darts line 422
63. theorem OAI.BinPackingGames.Foundations.PCP.RoundSize.output_total_le line 448
64. def OAI.BinPackingGames.Foundations.PCP.RoundGap.poweredLower line 462
65. theorem OAI.BinPackingGames.Foundations.PCP.RoundGap.poweredLower_nonnegative line 466
66. theorem OAI.BinPackingGames.Foundations.PCP.RoundGap.powered_count_gap line 474
67. theorem OAI.BinPackingGames.Foundations.PCP.RoundGap.amplifies line 502
68. abbrev OAI.BinPackingGames.Foundations.PCP.PCPIteration.Label line 522
69. abbrev OAI.BinPackingGames.Foundations.PCP.PCPIteration.Graph line 523
70. abbrev OAI.BinPackingGames.Foundations.PCP.PCPIteration.Addresses line 524
71. def OAI.BinPackingGames.Foundations.PCP.PCPIteration.step line 526
72. def OAI.BinPackingGames.Foundations.PCP.PCPIteration.run line 530
73. def OAI.BinPackingGames.Foundations.PCP.PCPIteration.initial line 533
74. def OAI.BinPackingGames.Foundations.PCP.PCPIteration.iterationCount line 535
75. def OAI.BinPackingGames.Foundations.PCP.PCPIteration.output line 537
76. def OAI.BinPackingGames.Foundations.PCP.PCPIteration.polynomialDegree line 540
77. def OAI.BinPackingGames.Foundations.PCP.PCPIteration.finalClauseGap line 542
78. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.finalClauseGap_positive line 544
79. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.sizeFactor_le_power line 548
80. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.initial_satisfiable_iff line 551
81. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.initial_size_positive line 555
82. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.initial_size_bound line 558
83. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.step_completeness line 566
84. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.step_gap line 570
85. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.step_size line 574
86. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.run_completeness line 578
87. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.run_gap line 584
88. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.run_size line 590
89. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.output_completeness line 596
90. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.output_gap line 602
91. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.output_satisfiable_iff line 612
92. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.output_size_polynomial line 622
93. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.output_size_clause_bound line 629
94. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.output_count_gap line 637
95. def OAI.BinPackingGames.Foundations.PCP.PCPIteration.finalCNF line 661
96. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.finalCNF_satisfiable_iff line 664
97. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.finalCNF_clause_count line 669
98. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.finalCNF_variable_count line 673
99. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.finalCNF_nonempty line 677
100. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.finalCNF_gap line 684
101. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.finalCNF_clauseGap line 696
102. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.finalCNF_total_size line 702
103. theorem OAI.BinPackingGames.Foundations.PCP.PCPIteration.finalCNF_polynomial_size line 719