OAI/Computability/DirectedFeedback/Encoding/PreprocessingOverlayTables.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts line 12
2. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inl_val line 14
3. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inr_val line 17
4. def OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts line 20
5. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_false_val line 23
6. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_true_val line 27
7. def OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.materialize line 31
8. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize line 44
9. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize_image line 55
10. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.accepts_materialize line 62
11. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.constraintGraph_ext_inline_PreprocessingOverlayTables line 69
12. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.baseGraph_materialize line 83
13. def OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.overlay line 99
14. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_old line 104
15. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_expander line 111
16. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_old line 118
17. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_expander line 125
18. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.overlay_semantics line 131
19. def OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.lazy line 139
20. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_false line 142
21. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_true line 148
22. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_false line 155
23. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_true line 161
24. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingOverlayTables.lazy_semantics line 168
25. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.dart_rejection_count_le line 181
26. def OAI.DFVSGames.Foundations.PCP.CloudRounding.colorSet line 230
27. def OAI.DFVSGames.Foundations.PCP.CloudRounding.minoritySet line 233
28. def OAI.DFVSGames.Foundations.PCP.CloudRounding.directedCut line 236
29. def OAI.DFVSGames.Foundations.PCP.CloudRounding.disagreementSet line 239
30. abbrev OAI.DFVSGames.Foundations.PCP.CloudRounding.Nonmajor line 242
31. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.exists_max_color line 245
32. def OAI.DFVSGames.Foundations.PCP.CloudRounding.majority line 252
33. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.majority_maximal line 256
34. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.nonchosen_color_twice_le line 262
35. def OAI.DFVSGames.Foundations.PCP.CloudRounding.minorityEquiv line 281
36. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.minority_card_eq_sum line 298
37. def OAI.DFVSGames.Foundations.PCP.CloudRounding.minorityCutEmbedding line 303
38. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.minority_cut_sum_le line 329
39. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.minority_expansion_bound line 336
40. def OAI.DFVSGames.Foundations.PCP.CloudRounding.mismatchSet line 366
41. def OAI.DFVSGames.Foundations.PCP.CloudRounding.copiedRejectionCount line 370
42. def OAI.DFVSGames.Foundations.PCP.CloudRounding.innerDisagreementSet line 373
43. def OAI.DFVSGames.Foundations.PCP.CloudRounding.roundLabels line 377
44. def OAI.DFVSGames.Foundations.PCP.CloudRounding.mismatchFiberEquiv line 381
45. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.mismatch_card_eq_sum line 399
46. def OAI.DFVSGames.Foundations.PCP.CloudRounding.disagreementFiberEquiv line 406
47. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.disagreement_card_eq_sum line 428
48. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.rounded_mismatch_expansion line 436
49. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.rounded_endpoint_bound line 453
50. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.copied_satisfied_inl line 460
51. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.copied_satisfied_inr line 466
52. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.replacement_rejection_split line 473
53. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.replacement_soundness line 485
54. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.padded_replacement_soundness line 501
55. theorem OAI.DFVSGames.Foundations.PCP.CloudRounding.combine_counts line 516
56. def OAI.DFVSGames.Foundations.PCP.SpectralCut.indicator line 546
57. theorem OAI.DFVSGames.Foundations.PCP.SpectralCut.mean_indicator line 548
58. theorem OAI.DFVSGames.Foundations.PCP.SpectralCut.energy_indicator line 556
59. theorem OAI.DFVSGames.Foundations.PCP.SpectralCut.indicator_nonnegative line 564
60. def OAI.DFVSGames.Foundations.PCP.SpectralCut.cut line 571
61. theorem OAI.DFVSGames.Foundations.PCP.SpectralCut.cut_density_eq line 579
62. theorem OAI.DFVSGames.Foundations.PCP.SpectralCut.cut_density_ge_variance line 601
63. theorem OAI.DFVSGames.Foundations.PCP.SpectralCut.cut_density_ge_quarter line 620
64. theorem OAI.DFVSGames.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree line 636
65. theorem OAI.DFVSGames.Foundations.PCP.SpectralCut.degree_mul_card_le_four_cut line 654
66. theorem OAI.DFVSGames.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree_of_card_le_half line 663
67. theorem OAI.DFVSGames.Foundations.PCP.SpectralCut.cut_card_ge_twice line 670
68. abbrev OAI.DFVSGames.Foundations.PCP.Regularization.Vertex line 698
69. abbrev OAI.DFVSGames.Foundations.PCP.Regularization.Port line 699
70. def OAI.DFVSGames.Foundations.PCP.Regularization.degree line 701
71. theorem OAI.DFVSGames.Foundations.PCP.Regularization.degree_eq line 703
72. theorem OAI.DFVSGames.Foundations.PCP.Regularization.degree_positive line 706
73. def OAI.DFVSGames.Foundations.PCP.Regularization.cloudEquiv line 708
74. def OAI.DFVSGames.Foundations.PCP.Regularization.cloudGraph line 714
75. theorem OAI.DFVSGames.Foundations.PCP.Regularization.cloudGraph_of_pos line 725
76. theorem OAI.DFVSGames.Foundations.PCP.Regularization.cloudGraph_certificate_of_pos line 733
77. theorem OAI.DFVSGames.Foundations.PCP.Regularization.cloud_expansion line 742
78. def OAI.DFVSGames.Foundations.PCP.Regularization.portGraph line 757
79. def OAI.DFVSGames.Foundations.PCP.Regularization.graph line 760
80. theorem OAI.DFVSGames.Foundations.PCP.Regularization.graph_tail line 765
81. theorem OAI.DFVSGames.Foundations.PCP.Regularization.graph_reverse line 769
82. def OAI.DFVSGames.Foundations.PCP.Regularization.degreeEquiv line 772
83. theorem OAI.DFVSGames.Foundations.PCP.Regularization.fixed_degree line 784
84. theorem OAI.DFVSGames.Foundations.PCP.Regularization.vertex_count_le line 789
85. theorem OAI.DFVSGames.Foundations.PCP.Regularization.dart_count line 794
86. theorem OAI.DFVSGames.Foundations.PCP.Regularization.dart_count_le line 799
87. def OAI.DFVSGames.Foundations.PCP.Regularization.liftLabel line 809
88. theorem OAI.DFVSGames.Foundations.PCP.Regularization.lift_rejectionCount line 814
89. theorem OAI.DFVSGames.Foundations.PCP.Regularization.completeness line 819
90. def OAI.DFVSGames.Foundations.PCP.Regularization.roundLabels line 824
91. theorem OAI.DFVSGames.Foundations.PCP.Regularization.soundness line 827
92. theorem OAI.DFVSGames.Foundations.PCP.Regularization.exists_rounding line 832
93. theorem OAI.DFVSGames.Foundations.PCP.Regularization.soundness_of_uniform_lower_bound line 836