OAI/Computability/UniqueGames/Reduction/ActualGame.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Actual finite translation game of Definition 4.6. All questions, linear maps, noise indices and linear functionals occur once in the outcome list. Equal noise vectors retain their index multiplicity.

  1. def OAI.UniqueGamesTheorem.Reduction.ActualGame.names line 25
  2. def OAI.UniqueGamesTheorem.Reduction.ActualGame.rhs line 29
  3. abbrev OAI.UniqueGamesTheorem.Reduction.ActualGame.Question line 31
  4. abbrev OAI.UniqueGamesTheorem.Reduction.ActualGame.Map line 32
  5. abbrev OAI.UniqueGamesTheorem.Reduction.ActualGame.Dual line 33
  6. abbrev OAI.UniqueGamesTheorem.Reduction.ActualGame.Query line 34
  7. instance OAI.UniqueGamesTheorem.Reduction.ActualGame.mapFintype line 36
  8. instance OAI.UniqueGamesTheorem.Reduction.ActualGame.dualFintype line 40
  9. def OAI.UniqueGamesTheorem.Reduction.ActualGame.canonical line 44
  10. abbrev OAI.UniqueGamesTheorem.Reduction.ActualGame.Vertex line 47
  11. abbrev OAI.UniqueGamesTheorem.Reduction.ActualGame.TwoSidedVertex line 48
  12. def OAI.UniqueGamesTheorem.Reduction.ActualGame.vertex line 50
  13. def OAI.UniqueGamesTheorem.Reduction.ActualGame.offset line 53
  14. def OAI.UniqueGamesTheorem.Reduction.ActualGame.shiftQuery line 56
  15. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.canonical_shiftQuery line 60
  16. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.vertex_shiftQuery line 66
  17. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.offset_shiftQuery line 72
  18. def OAI.UniqueGamesTheorem.Reduction.ActualGame.vertexCount line 77
  19. def OAI.UniqueGamesTheorem.Reduction.ActualGame.vertexEncoding line 80
  20. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.vertexCount_eq_twice line 84
  21. abbrev OAI.UniqueGamesTheorem.Reduction.ActualGame.Outcome line 89

    Source documentation

    Each product element is a separate edge occurrence.

    abbrev Outcome (S : Source) (k : Nat) {s d : Nat} (g : SplitGadget s d) :=
…
  22. def OAI.UniqueGamesTheorem.Reduction.ActualGame.leftQuery line 92
  23. def OAI.UniqueGamesTheorem.Reduction.ActualGame.rightQuery line 95
  24. def OAI.UniqueGamesTheorem.Reduction.ActualGame.edge line 99
  25. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.edge_source_ne_target line 106
  26. def OAI.UniqueGamesTheorem.Reduction.ActualGame.outcomes line 114
  27. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.mem_outcomes line 117
  28. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.outcomes_nodup line 121
  29. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.outcomes_length line 124
  30. def OAI.UniqueGamesTheorem.Reduction.ActualGame.outputInstance line 128
  31. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.outputInstance_constraints_length line 140
  32. def OAI.UniqueGamesTheorem.Reduction.ActualGame.sideLabel line 145
  33. def OAI.UniqueGamesTheorem.Reduction.ActualGame.labelingOf line 150
  34. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.sideLabel_labelingOf line 156
  35. def OAI.UniqueGamesTheorem.Reduction.ActualGame.unfolded line 162
  36. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.unfolded_equivariant line 167
  37. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.edge_satisfied_iff line 177
  38. def OAI.UniqueGamesTheorem.Reduction.ActualGame.acceptanceProbability line 191
  39. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.acceptanceProbability_eq_test line 196
  40. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.countSatisfied_map line 208
  41. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.countSatisfied_eq_sum line 216
  42. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.acceptanceProbability_eq_count line 225

    Source documentation

    The expectation is exactly the satisfied fraction of the explicit edge list.

    theorem acceptanceProbability_eq_count (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (labeling : Fin (vertexCount S k s d) → Fin (2^s)) :
    acceptanceProbability S k g labeling =
      (countSatisfied labeling (outputInstance S k g).constraints : ℚ) /
        (outputInstance S k g).constraints.length := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.ActualGame.vertexCount, OAI.UniqueGamesTheorem.Reduction.ActualGame.acceptanceProbability, OAI.UniqueGamesTheorem.Reduction.ActualGame.outputInstance

  43. def OAI.UniqueGamesTheorem.Reduction.ActualGame.orbitBodyDecidableEq line 237
  44. def OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitBodies line 242
  45. def OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitVertexCount line 247
  46. def OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitVertexEncoding line 250
  47. def OAI.UniqueGamesTheorem.Reduction.ActualGame.semanticToExplicitVertices line 258
  48. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.semanticToExplicitVertices_apply line 262
  49. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitVertexCount_eq line 268
  50. def OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitEdge line 272
  51. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitEdge_eq_rename line 279
  52. def OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitOutcomes line 286
  53. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitOutcomes_nodup line 290
  54. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.mem_explicitOutcomes line 295
  55. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitOutcomes_perm_outcomes line 300
  56. def OAI.UniqueGamesTheorem.Reduction.ActualGame.outputInstanceWithEnumeration line 310

    Source documentation

    This construction computes its vertex numbering, all outcomes, and every forward/inverse permutation entry from the explicitly supplied finite data.

    def outputInstanceWithEnumeration (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g) : Foundations.Target.Instance (2^s) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Instance

  57. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.outputInstanceWithEnumeration_length line 323
  58. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.explicitConstraints_perm_renamed line 330
  59. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.completeAt_outputInstanceWithEnumeration_iff line 339
  60. theorem OAI.UniqueGamesTheorem.Reduction.ActualGame.soundAt_outputInstanceWithEnumeration_iff line 347