OAI/Computability/UniqueGames/Games/UniformTarget.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.copy_length line 14
2. def OAI.UniqueGamesTheorem.Explicit.UniformTarget.construct line 22
3. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.vertices line 30
4. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.edge_count line 33
5. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.count_append line 37
6. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.count_copies line 42
7. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.count line 52
8. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.maxSatisfied line 57
9. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.value line 71
10. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.mem_original line 81
11. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.translations line 88
12. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.flatMap_copies line 95
13. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.encode_copies line 103
14. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.gameWords_construct line 112

    Source documentation

    The complete output keeps the two first headers and scales the edge count.

    theorem gameWords_construct {q : Nat} (C : Nat) (hC : 0 < C) (g : Instance q) :
        gameWords (construct C hC g) =
          [g.vertices, q, C * g.constraints.length] ++
            copyMajor C (g.constraints.flatMap constraintWords) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.UniformTarget.construct

15. theorem OAI.UniqueGamesTheorem.Explicit.UniformTarget.gameBits_construct line 120