OAI/Computability/MaxCut/PCP/SpectralCut.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Foundations.PCP.SpectralCut.indicator line 18
2. theorem OAI.MaxCutGames.Foundations.PCP.SpectralCut.mean_indicator line 20
3. theorem OAI.MaxCutGames.Foundations.PCP.SpectralCut.energy_indicator line 28
4. theorem OAI.MaxCutGames.Foundations.PCP.SpectralCut.indicator_nonnegative line 36
5. def OAI.MaxCutGames.Foundations.PCP.SpectralCut.cut line 43
6. theorem OAI.MaxCutGames.Foundations.PCP.SpectralCut.cut_density_eq line 51

   Source documentation

   The normalized cut count is exactly mean minus one-step correlation.

   theorem cut_density_eq (S : Finset V) :
       ((cut G S).card : ℝ) / (Fintype.card (V × D) : ℝ) =
         mean (indicator S) - correlation (indicator S) (averagingOperator G (indicator S)) := by
   …

   Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralCut.cut, OAI.MaxCutGames.Foundations.PCP.SpectralCut.indicator

7. theorem OAI.MaxCutGames.Foundations.PCP.SpectralCut.cut_density_ge_variance line 73
8. theorem OAI.MaxCutGames.Foundations.PCP.SpectralCut.cut_density_ge_quarter line 92
9. theorem OAI.MaxCutGames.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree line 109

   Source documentation

   The real cardinal estimate before removing denominators.

   theorem cut_card_ge_quarter_degree
       (certificate : SpectralCertificate G (1/2)) (S : Finset V)
       (hsmall : 2 * S.card ≤ Fintype.card V) :
       (Fintype.card D : ℝ) * (S.card : ℝ) / 4 ≤ ((cut G S).card : ℝ) := by
   …

   Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralCut.cut

10. theorem OAI.MaxCutGames.Foundations.PCP.SpectralCut.degree_mul_card_le_four_cut line 127
11. theorem OAI.MaxCutGames.Foundations.PCP.SpectralCut.cut_card_ge_quarter_degree_of_card_le_half line 136
12. theorem OAI.MaxCutGames.Foundations.PCP.SpectralCut.cut_card_ge_twice line 145

    Source documentation

    The natural-number expansion used in cloud rounding. Empty vertex sets are included; a degree of at least eight supplies the nonempty port type.

    theorem cut_card_ge_twice (G : PortGraph V D)
        (certificate : SpectralCertificate G (1/2)) (hdegree : 8 ≤ Fintype.card D)
        (S : Finset V) (hsmall : 2 * S.card ≤ Fintype.card V) :
        2 * S.card ≤ (cut G S).card := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralCut.cut

13. abbrev OAI.MaxCutGames.Foundations.PCP.Regularization.Vertex line 179
14. abbrev OAI.MaxCutGames.Foundations.PCP.Regularization.Port line 180
15. def OAI.MaxCutGames.Foundations.PCP.Regularization.degree line 183

    Source documentation

    The degree is one absolute constant, independent of the input graph.

    def degree : Nat := Fintype.card Port

    Mentions: OAI.MaxCutGames.Foundations.PCP.Regularization.Port

16. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.degree_eq line 185
17. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.degree_positive line 188
18. def OAI.MaxCutGames.Foundations.PCP.Regularization.cloudEquiv line 191

    Source documentation

    A positive padded cloud has exactly the size of one explicit family member.

    def cloudEquiv (G : ConstraintGraph V E A) (v : V)
        (hk : 0 < Fintype.card (Cloud G v)) :
        ExpanderFamily.Vertex (ExpanderFamily.level (Fintype.card (Cloud G v))) ≃
          Cloud (paddedGraph G (CloudPadding.dummy G)) v :=
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.Vertex, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.level, OAI.MaxCutGames.Foundations.PCP.CloudPadding.dummy

19. def OAI.MaxCutGames.Foundations.PCP.Regularization.cloudGraph line 198

    Source documentation

    Empty clouds use the empty rotation; every other cloud uses the proved family.

    def cloudGraph (G : ConstraintGraph V E A) (v : V) :
        PortGraph (Cloud (paddedGraph G (CloudPadding.dummy G)) v) ExpanderFamily.Port :=
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.CloudPadding.dummy, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.Port

20. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.cloudGraph_of_pos line 209
21. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.cloudGraph_certificate_of_pos line 217
22. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.cloud_expansion line 226

    Source documentation

    The exact expansion premise required by the checked finite rounding theorem.

    theorem cloud_expansion (G : ConstraintGraph V E A) (v : V)
        (S : Finset (Cloud (paddedGraph G (CloudPadding.dummy G)) v))
        (hsmall : S.card ≤
          Fintype.card (Cloud (paddedGraph G (CloudPadding.dummy G)) v) / 2) :
        2 * S.card ≤
          (CloudRounding.directedCut (fun ed => ((cloudGraph G v).rot ed).1) S).card := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.CloudPadding.dummy, OAI.MaxCutGames.Foundations.PCP.CloudRounding.directedCut, OAI.MaxCutGames.Foundations.PCP.Regularization.cloudGraph

23. def OAI.MaxCutGames.Foundations.PCP.Regularization.portGraph line 241
24. def OAI.MaxCutGames.Foundations.PCP.Regularization.graph line 245

    Source documentation

    The actual constraint graph, with its equality and inherited original tests.

    def graph (G : ConstraintGraph V E A) :
        ConstraintGraph (Vertex G) (Vertex G × Port) A :=
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Regularization.Vertex, OAI.MaxCutGames.Foundations.PCP.Regularization.Port

25. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.graph_tail line 250
26. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.graph_reverse line 254
27. def OAI.MaxCutGames.Foundations.PCP.Regularization.degreeEquiv line 258

    Source documentation

    The outgoing darts at each new vertex are exactly its fixed port alphabet.

    def degreeEquiv (G : ConstraintGraph V E A) (v : Vertex G) :
        Cloud (graph G) v ≃ Port where
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Regularization.Vertex, OAI.MaxCutGames.Foundations.PCP.Regularization.graph, OAI.MaxCutGames.Foundations.PCP.Regularization.Port

28. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.fixed_degree line 270
29. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.vertex_count_le line 275
30. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.dart_count line 280
31. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.dart_count_le line 285
32. def OAI.MaxCutGames.Foundations.PCP.Regularization.liftLabel line 295
33. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.lift_rejectionCount line 300

    Source documentation

    Completeness preserves the absolute rejection count exactly.

    theorem lift_rejectionCount (G : ConstraintGraph V E A) (labeling : V → A) :
        (graph G).rejectionCount (liftLabel G labeling) = G.rejectionCount labeling :=
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Regularization.graph, OAI.MaxCutGames.Foundations.PCP.Regularization.liftLabel

34. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.completeness line 305
35. def OAI.MaxCutGames.Foundations.PCP.Regularization.roundLabels line 310
36. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.soundness line 314

    Source documentation

    Actual regularization soundness with no remaining expansion or rounding premise.

    theorem soundness [Nonempty A] (G : ConstraintGraph V E A) (ell : Vertex G → A) :
        G.rejectionCount (roundLabels G ell) ≤ (graph G).rejectionCount ell :=
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Regularization.Vertex, OAI.MaxCutGames.Foundations.PCP.Regularization.roundLabels, OAI.MaxCutGames.Foundations.PCP.Regularization.graph

37. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.exists_rounding line 319
38. theorem OAI.MaxCutGames.Foundations.PCP.Regularization.soundness_of_uniform_lower_bound line 323
39. theorem OAI.MaxCutGames.Foundations.PCP.LazySpectral.half_sum_sq_le line 344
40. theorem OAI.MaxCutGames.Foundations.PCP.LazySpectral.lazy_energy_le_average line 349

    Source documentation

    Lazification averages the input and one actual graph step, so its energy is at most the corresponding average of the two energies.

    theorem lazy_energy_le_average [Fintype V] [Fintype D] [Nonempty D]
        (G : PortGraph V D) (f : V → ℝ) :
        energy (averagingOperator (lazyGraph G) f) ≤
          (energy f + energy (averagingOperator G f)) / 2 := by
    …

41. theorem OAI.MaxCutGames.Foundations.PCP.LazySpectral.lazy_energy_bound line 373

    Source documentation

    The concrete lazy graph inherits a squared-energy bound from an actual certificate for its underlying graph.

    theorem lazy_energy_bound [Fintype V] [Fintype D] [Nonempty D]
        (G : PortGraph V D) (lambda : ℝ) (hG : SpectralCertificate G lambda)
        (f : V → ℝ) (hf : mean f = 0) :
        energy (averagingOperator (lazyGraph G) f) ≤
          ((1 + lambda ^ 2) / 2) * energy f := by
    …

42. theorem OAI.MaxCutGames.Foundations.PCP.LazySpectral.lazy_certificate_31_32 line 388

    Source documentation

    An actual 7/8 certificate gives the stated 31/32 certificate after lazification: its intermediate squared-energy factor is 113/128.

    theorem lazy_certificate_31_32 [Fintype V] [Fintype D] [Nonempty D]
        (G : PortGraph V D) (hG : SpectralCertificate G (7 / 8)) :
        SpectralCertificate (lazyGraph G) (31 / 32) where
    …

43. abbrev OAI.MaxCutGames.Foundations.PCP.Preprocessing.Vertex line 411
44. abbrev OAI.MaxCutGames.Foundations.PCP.Preprocessing.OverlayPort line 412
45. abbrev OAI.MaxCutGames.Foundations.PCP.Preprocessing.Port line 413
46. def OAI.MaxCutGames.Foundations.PCP.Preprocessing.degree line 415
47. def OAI.MaxCutGames.Foundations.PCP.Preprocessing.sizeFactor line 416
48. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.card_lazy_sum_inline_Preprocessing line 418
49. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.doubled_add_inline_Preprocessing line 423
50. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.degree_eq_card line 425
51. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.degree_positive line 434
52. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.sizeFactor_positive line 438
53. def OAI.MaxCutGames.Foundations.PCP.Preprocessing.paddedGraph line 444

    Source documentation

    Whole-graph padding retains each original regularized constraint.

    def paddedGraph (G : ConstraintGraph V E A) :
        ConstraintGraph (Vertex G) (Vertex G × Regularization.Port) A :=
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Preprocessing.Vertex, OAI.MaxCutGames.Foundations.PCP.Regularization.Port

54. def OAI.MaxCutGames.Foundations.PCP.Preprocessing.overlayExpander line 449

    Source documentation

    The overlay expander is transported to this exact padded vertex set.

    def overlayExpander (G : ConstraintGraph V E A) :
        PortGraph (Vertex G) ExpanderFamily.Port :=
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Preprocessing.Vertex, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.Port

55. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.overlayExpander_certificate line 456
56. def OAI.MaxCutGames.Foundations.PCP.Preprocessing.overlayGraph line 460
57. def OAI.MaxCutGames.Foundations.PCP.Preprocessing.graph line 464
58. def OAI.MaxCutGames.Foundations.PCP.Preprocessing.portGraph line 468
59. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.graph_tail line 472
60. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.graph_reverse line 475
61. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.accepts_reverse line 479
62. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.portGraph_eq_lazyGraph line 484
63. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.overlayGraph_certificate line 488
64. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.spectral_certificate line 498

    Source documentation

    The actual output operator has one fixed spectral contraction factor.

    theorem spectral_certificate (G : ConstraintGraph V E A) :
        SpectralCertificate (portGraph G) (31 / 32 : ℝ) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Preprocessing.portGraph

65. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.vertex_count_le line 505
66. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.dart_count line 515
67. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.dart_count_le line 521
68. def OAI.MaxCutGames.Foundations.PCP.Preprocessing.liftLabel line 529
69. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.lift_rejectionCount line 535

    Source documentation

    Lifting any original assignment preserves its absolute rejection count.

    theorem lift_rejectionCount (G : ConstraintGraph V E A) (labeling : V → A) :
        (graph G).rejectionCount (liftLabel G labeling) = G.rejectionCount labeling := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Preprocessing.graph, OAI.MaxCutGames.Foundations.PCP.Preprocessing.liftLabel

70. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.completeness line 547
71. def OAI.MaxCutGames.Foundations.PCP.Preprocessing.roundLabels line 554
72. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.soundness line 560

    Source documentation

    Rounding an arbitrary output assignment gives an original assignment with no more rejected darts. There are no expansion or rounding hypotheses.

    theorem soundness (G : ConstraintGraph V E A) (labeling : Vertex G → A) :
        G.rejectionCount (roundLabels G labeling) ≤ (graph G).rejectionCount labeling := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Preprocessing.Vertex, OAI.MaxCutGames.Foundations.PCP.Preprocessing.roundLabels, OAI.MaxCutGames.Foundations.PCP.Preprocessing.graph

73. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.satisfiable_iff line 573
74. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.gap_transfer line 587

    Source documentation

    The quantitative lower bound used by each amplification iteration. The single constant sizeFactor is independent of the alphabet and input graph.

    theorem gap_transfer (G : ConstraintGraph V E A) (epsilon : ℚ) (he : 0 ≤ epsilon)
        (lower : ∀ labeling : V → A,
          epsilon * Fintype.card E ≤ (G.rejectionCount labeling : ℚ))
        (labeling : Vertex G → A) :
        (epsilon / sizeFactor) * Fintype.card (Vertex G × Port) ≤
          ((graph G).rejectionCount labeling : ℚ) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Preprocessing.Vertex, OAI.MaxCutGames.Foundations.PCP.Preprocessing.sizeFactor, OAI.MaxCutGames.Foundations.PCP.Preprocessing.Port, OAI.MaxCutGames.Foundations.PCP.Preprocessing.graph

75. theorem OAI.MaxCutGames.Foundations.PCP.Preprocessing.gap_transfer_real line 605

    Source documentation

    The same actual counting guarantee in the real normalization used for walk amplification. No rational approximation premise is needed.

    theorem gap_transfer_real (G : ConstraintGraph V E A) (epsilon : ℝ) (he : 0 ≤ epsilon)
        (lower : ∀ labeling : V → A,
          epsilon * Fintype.card E ≤ (G.rejectionCount labeling : ℝ))
        (labeling : Vertex G → A) :
        (epsilon / sizeFactor) * Fintype.card (Vertex G × Port) ≤
          ((graph G).rejectionCount labeling : ℝ) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.Preprocessing.Vertex, OAI.MaxCutGames.Foundations.PCP.Preprocessing.sizeFactor, OAI.MaxCutGames.Foundations.PCP.Preprocessing.Port, OAI.MaxCutGames.Foundations.PCP.Preprocessing.graph

76. abbrev OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.BaseTable line 638
77. def OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.degree line 640
78. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.degree_eq line 642
79. def OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.regularVertices line 647
80. def OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.vertices line 648
81. def OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.padded line 650
82. def OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.overlayFamily line 655
83. def OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.preprocess line 660
84. def OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.output line 665
85. def OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.graphTable line 668
86. def OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.outputBits line 671
87. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.regularVertices_ge_darts line 674
88. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.regularVertices_le line 678
89. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.vertices_positive line 681
90. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.vertices_le_of_positive line 684
91. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.vertices_eq_one_of_no_darts line 694
92. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.vertices_le line 700

    Source documentation

    The total algorithm also has a uniform data bound on empty inputs.

    theorem vertices_le (t : GraphTables.Table) :
        vertices t ≤ ExpanderFamily.growth ^ 2 * (t.darts + 1) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.vertices, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.growth

93. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.darts_eq line 710
94. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.darts_le line 713
95. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.vertices_le_inputBits line 721
96. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTables.darts_le_inputBits line 726