OAI/Computability/UniqueGames/PCP/Preprocessing.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.Vertex line 17
2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.OverlayPort line 18
3. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.Port line 19
4. def OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.degree line 21
5. def OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.sizeFactor line 22
6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.card_lazy_sum line 24
7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.doubled_add line 29
8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.degree_eq_card line 31
9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.degree_positive line 40
10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.sizeFactor_positive line 44
11. def OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.paddedGraph line 50

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.Regularization.Port

12. def OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.overlayExpander line 55

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.Port

13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.overlayExpander_certificate line 62
14. def OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.overlayGraph line 66
15. def OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.graph line 70
16. def OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.portGraph line 74
17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.graph_tail line 78
18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.graph_reverse line 81
19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.accepts_reverse line 85
20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.portGraph_eq_lazyGraph line 90
21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.overlayGraph_certificate line 94
22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.spectral_certificate line 104

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.portGraph

23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.vertex_count_le line 110
24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.dart_count line 120
25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.dart_count_le line 125
26. def OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.liftLabel line 133
27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.lift_rejectionCount line 138

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.graph, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.liftLabel

28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.completeness line 149
29. def OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.roundLabels line 156
30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.soundness line 162

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.roundLabels, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.graph

31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.satisfiable_iff line 175
32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.gap_transfer line 189

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.sizeFactor, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.Port, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.graph

33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.gap_transfer_real line 207

    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.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.sizeFactor, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.Port, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.graph