OAI/Computability/MinUncut/PCP/SpectralCut.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.PCP.SpectralCut.indicator line 16
  2. theorem OAI.MinUncutGames.Foundations.PCP.SpectralCut.mean_indicator line 18
  3. theorem OAI.MinUncutGames.Foundations.PCP.SpectralCut.energy_indicator line 26
  4. theorem OAI.MinUncutGames.Foundations.PCP.SpectralCut.indicator_nonnegative line 34
  5. def OAI.MinUncutGames.Foundations.PCP.SpectralCut.cut line 41
  6. theorem OAI.MinUncutGames.Foundations.PCP.SpectralCut.cut_density_eq line 48
  7. theorem OAI.MinUncutGames.Foundations.PCP.SpectralCut.cut_density_ge_variance line 70
  8. theorem OAI.MinUncutGames.Foundations.PCP.SpectralCut.cut_density_ge_quarter line 89
  9. theorem OAI.MinUncutGames.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree line 105
  10. theorem OAI.MinUncutGames.Foundations.PCP.SpectralCut.degree_mul_card_le_four_cut line 122
  11. theorem OAI.MinUncutGames.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree_of_card_le_half line 131
  12. theorem OAI.MinUncutGames.Foundations.PCP.SpectralCut.cut_card_ge_twice line 138
  13. abbrev OAI.MinUncutGames.Foundations.PCP.Regularization.Vertex line 163
  14. abbrev OAI.MinUncutGames.Foundations.PCP.Regularization.Port line 164
  15. def OAI.MinUncutGames.Foundations.PCP.Regularization.degree line 166
  16. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.degree_eq line 168
  17. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.degree_positive line 171
  18. def OAI.MinUncutGames.Foundations.PCP.Regularization.cloudEquiv line 173
  19. def OAI.MinUncutGames.Foundations.PCP.Regularization.cloudGraph line 179
  20. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.cloudGraph_of_pos line 190
  21. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.cloudGraph_certificate_of_pos line 198
  22. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.cloud_expansion line 206
  23. def OAI.MinUncutGames.Foundations.PCP.Regularization.portGraph line 221
  24. def OAI.MinUncutGames.Foundations.PCP.Regularization.graph line 224
  25. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.graph_tail line 229
  26. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.graph_reverse line 233
  27. def OAI.MinUncutGames.Foundations.PCP.Regularization.degreeEquiv line 236
  28. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.fixed_degree line 248
  29. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.vertex_count_le line 253
  30. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.dart_count line 258
  31. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.dart_count_le line 263
  32. def OAI.MinUncutGames.Foundations.PCP.Regularization.liftLabel line 273
  33. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.lift_rejectionCount line 277
  34. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.completeness line 282
  35. def OAI.MinUncutGames.Foundations.PCP.Regularization.roundLabels line 287
  36. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.soundness line 290
  37. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.exists_rounding line 295
  38. theorem OAI.MinUncutGames.Foundations.PCP.Regularization.soundness_of_uniform_lower_bound line 299
  39. theorem OAI.MinUncutGames.Foundations.PCP.LazySpectral.half_sum_sq_le line 315
  40. theorem OAI.MinUncutGames.Foundations.PCP.LazySpectral.lazy_energy_le_average line 318
  41. theorem OAI.MinUncutGames.Foundations.PCP.LazySpectral.lazy_energy_bound line 340
  42. theorem OAI.MinUncutGames.Foundations.PCP.LazySpectral.lazy_certificate_31_32 line 353
  43. abbrev OAI.MinUncutGames.Foundations.PCP.Preprocessing.Vertex line 376
  44. abbrev OAI.MinUncutGames.Foundations.PCP.Preprocessing.OverlayPort line 377
  45. abbrev OAI.MinUncutGames.Foundations.PCP.Preprocessing.Port line 378
  46. def OAI.MinUncutGames.Foundations.PCP.Preprocessing.degree line 380
  47. def OAI.MinUncutGames.Foundations.PCP.Preprocessing.sizeFactor line 381
  48. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.card_lazy_sum line 383
  49. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.doubled_add line 388
  50. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.degree_eq_card line 390
  51. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.degree_positive line 399
  52. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.sizeFactor_positive line 403
  53. def OAI.MinUncutGames.Foundations.PCP.Preprocessing.paddedGraph line 408
  54. def OAI.MinUncutGames.Foundations.PCP.Preprocessing.overlayExpander line 412
  55. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.overlayExpander_certificate line 419
  56. def OAI.MinUncutGames.Foundations.PCP.Preprocessing.overlayGraph line 423
  57. def OAI.MinUncutGames.Foundations.PCP.Preprocessing.graph line 427
  58. def OAI.MinUncutGames.Foundations.PCP.Preprocessing.portGraph line 431
  59. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.graph_tail line 435
  60. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.graph_reverse line 438
  61. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.accepts_reverse line 442
  62. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.portGraph_eq_lazyGraph line 447
  63. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.overlayGraph_certificate line 451
  64. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.spectral_certificate line 460
  65. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.vertex_count_le line 466
  66. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.dart_count line 476
  67. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.dart_count_le line 481
  68. def OAI.MinUncutGames.Foundations.PCP.Preprocessing.liftLabel line 489
  69. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.lift_rejectionCount line 493
  70. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.completeness line 504
  71. def OAI.MinUncutGames.Foundations.PCP.Preprocessing.roundLabels line 511
  72. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.soundness line 515
  73. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.satisfiable_iff line 528
  74. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.gap_transfer line 540
  75. theorem OAI.MinUncutGames.Foundations.PCP.Preprocessing.gap_transfer_real line 556
  76. abbrev OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.BaseTable line 579
  77. def OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.degree line 581
  78. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.degree_eq line 583
  79. def OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.regularVertices line 588
  80. def OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.vertices line 589
  81. def OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.padded line 591
  82. def OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.overlayFamily line 596
  83. def OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.preprocess line 601
  84. def OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.output line 606
  85. def OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.graphTable line 609
  86. def OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.outputBits line 612
  87. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.regularVertices_ge_darts line 615
  88. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.regularVertices_le line 619
  89. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.vertices_positive line 622
  90. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.vertices_le_of_positive line 625
  91. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.vertices_eq_one_of_no_darts line 635
  92. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.vertices_le line 640
  93. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.darts_eq line 650
  94. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.darts_le line 653
  95. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.vertices_le_inputBits line 661
  96. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTables.darts_le_inputBits line 666
  97. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.internalDegree_ge_eight line 678
  98. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.baseDegree_ne_zero line 682
  99. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.resizeTable_certificate line 688
  100. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.familyCloudTable_certificate_of_pos line 695
  101. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.cloudGraphs_certificate_of_pos line 706
  102. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.cloud_expansion line 715
  103. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.roundLabels line 737
  104. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.soundness line 744
  105. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.exists_rounding line 755
  106. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.lift_rejectionCount line 764
  107. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.completeness line 770
  108. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_lower_bound line 792
  109. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_real_lower_bound line 801