OAI/Computability/MinUncut/PCP/GraphGap.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.rejectionCounts line 17
2. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.rejectionCounts_nonempty line 21
3. def OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.minimumRejections line 26
4. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.minimumRejections_le line 29
5. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.exists_minimizer line 34
6. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.le_minimumRejections_iff line 41
7. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.minimumRejections_le_card line 51
8. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.rejectionCount_eq_zero_iff line 58
9. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.minimumRejections_eq_zero_iff line 73
10. def OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.gap line 83
11. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.gap_nonnegative line 86
12. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.gap_le_one line 89
13. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.gap_eq_zero_iff line 95
14. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.le_gap_iff line 101
15. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.inverse_card_le_gap_of_unsatisfiable line 114
16. def OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.reindex line 128
17. def OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.labelingEquiv line 142
18. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.reindex_edgeSatisfied line 148
19. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.reindex_rejectionCount line 155
20. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.rejectionCounts_reindex line 179
21. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.minimumRejections_reindex line 196
22. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.gap_reindex line 202
23. theorem OAI.MinUncutGames.Foundations.PCP.ConstraintGraph.satisfiable_reindex line 208
24. def OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts line 221
25. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inl_val line 223
26. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inr_val line 226
27. def OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts line 229
28. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_false_val line 232
29. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_true_val line 236
30. def OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.materialize line 240
31. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize line 254
32. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize_image line 265
33. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.accepts_materialize line 272
34. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.constraintGraph_ext line 279
35. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.baseGraph_materialize line 293
36. def OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.overlay line 309
37. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_old line 314
38. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_expander line 321
39. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_old line 328
40. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_expander line 335
41. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.overlay_semantics line 341
42. def OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.lazy line 349
43. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_false line 352
44. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_true line 358
45. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_false line 365
46. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_true line 371
47. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingOverlayTables.lazy_semantics line 378
48. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.dart_rejection_count_le line 390
49. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.colorSet line 439
50. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.minoritySet line 442
51. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.directedCut line 445
52. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.disagreementSet line 448
53. abbrev OAI.MinUncutGames.Foundations.PCP.CloudRounding.Nonmajor line 451
54. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.exists_max_color line 454
55. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.majority line 461
56. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.majority_maximal line 465
57. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.nonchosen_color_twice_le line 470
58. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.minorityEquiv line 489
59. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.minority_card_eq_sum line 506
60. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.minorityCutEmbedding line 511
61. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.minority_cut_sum_le line 537
62. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.minority_expansion_bound line 544
63. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.mismatchSet line 574
64. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.copiedRejectionCount line 578
65. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.innerDisagreementSet line 581
66. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.roundLabels line 585
67. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.mismatchFiberEquiv line 589
68. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.mismatch_card_eq_sum line 607
69. def OAI.MinUncutGames.Foundations.PCP.CloudRounding.disagreementFiberEquiv line 614
70. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.disagreement_card_eq_sum line 636
71. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.rounded_mismatch_expansion line 644
72. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.rounded_endpoint_bound line 661
73. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.copied_satisfied_inl line 668
74. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.copied_satisfied_inr line 674
75. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.replacement_rejection_split line 680
76. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.replacement_soundness line 692
77. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.padded_replacement_soundness line 708
78. theorem OAI.MinUncutGames.Foundations.PCP.CloudRounding.combine_counts line 723