OAI/Computability/UniqueGames/PCP/VertexPadding.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.reverseFunction line 18

   Source documentation

   Original darts use the original reversal; dummy darts stay fixed.

   def reverseFunction (G : ConstraintGraph V (V × D) A) (extra : ℕ) :
       (V ⊕ Fin extra) × D → (V ⊕ Fin extra) × D
     | (Sum.inl v, d) => (Sum.inl (G.reverse (v, d)).1, (G.reverse (v, d)).2)
     | (Sum.inr w, d) => (Sum.inr w, d)

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph

2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.reverseFunction_involutive line 23
3. def OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.pad line 32

   Source documentation

   Actual regular padding by an arbitrary finite number of dummy vertices.

   def pad (G : ConstraintGraph V (V × D) A) (extra : ℕ) :
       ConstraintGraph (V ⊕ Fin extra) ((V ⊕ Fin extra) × D) A where
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph

4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.pad_tail line 50
5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.pad_reverse_inl line 53
6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.pad_reverse_inr line 58
7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.edgeSatisfied_inl line 62
8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.edgeSatisfied_inr line 73
9. def OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.extendLabeling line 77
10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.extendLabeling_inl line 80
11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.extendLabeling_inr line 83
12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.pad_satisfiable line 86
13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.satisfiable_of_pad line 94
14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.rejectionCount_eq_sum line 101
15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.pad_rejectionCount line 107

    Source documentation

    Exact counts for every padded labeling, without any condition on dummy labels.

    theorem pad_rejectionCount [Fintype V] [Fintype D]
        (G : ConstraintGraph V (V × D) A) (htail : G.tail = Prod.fst) (extra : ℕ)
        (labeling : V ⊕ Fin extra → A) :
        (pad G extra).rejectionCount labeling =
          G.rejectionCount (fun v => labeling (Sum.inl v)) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.pad

16. def OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.extraVertices line 121
17. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.Vertex line 123
18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.card_vertex line 125
19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.le_card_vertex line 129
20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.card_vertex_le line 133
21. def OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.familyVertexEquiv line 139

    Source documentation

    Exact coordinate bridge to the proved geometric family.

    noncomputable def familyVertexEquiv :
        Vertex V ≃ ExpanderFamily.Vertex (ExpanderFamily.level (Fintype.card V)) :=
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.level

22. def OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.paddedG line 147
23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.paddedG_tail line 150
24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.paddedG_rejectionCount line 153
25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.rejectionCount_eq line 160
26. def OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.liftLabel line 167
27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.liftLabel_inl line 170
28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.liftLabel_inr line 173
29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.rejectionCount_liftLabel line 177
30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.paddedG_satisfiable line 184
31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.card_padded_darts line 188
32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.VertexPadding.card_padded_darts_le line 192