OAI/Computability/MaxCut/Games/NoiseEnumeration.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

An explicit enumeration of noise indices, retaining repeated vector values. This additional data leaves SplitGadget unchanged and supplies an executable ordering for the edge list.

  1. structure OAI.MaxCutGames.Reduction.ActualSource.NoiseEnumeration line 16
  2. def OAI.MaxCutGames.Reduction.ActualSource.NoiseEnumeration.ofFintype line 25
  3. theorem OAI.MaxCutGames.Reduction.ActualSource.NoiseEnumeration.nonempty line 30
  4. theorem OAI.MaxCutGames.Reduction.ActualSource.NoiseEnumeration.perm_univ line 36
  5. theorem OAI.MaxCutGames.Reduction.ActualSource.NoiseEnumeration.length_eq_card line 42
  6. theorem OAI.MaxCutGames.Reduction.ActualSource.NoiseEnumeration.sum_eq_univ line 46
  7. theorem OAI.MaxCutGames.Reduction.ActualSource.NoiseEnumeration.average_eq_expect line 51

    Source documentation

    A list average over index occurrences is precisely the uniform finite law.

    theorem average_eq_expect (e : NoiseEnumeration g) (f : g.NoiseIndex → ℚ) :
    (e.indices.map f).sum / e.indices.length = Finset.univ.expect f := by
…

    Mentions: OAI.MaxCutGames.Reduction.ActualSource.NoiseEnumeration

  8. def OAI.MaxCutGames.Reduction.ActualGame.names line 69
  9. def OAI.MaxCutGames.Reduction.ActualGame.rhs line 73
  10. abbrev OAI.MaxCutGames.Reduction.ActualGame.Question line 75
  11. abbrev OAI.MaxCutGames.Reduction.ActualGame.Map line 76
  12. abbrev OAI.MaxCutGames.Reduction.ActualGame.Dual line 77
  13. abbrev OAI.MaxCutGames.Reduction.ActualGame.Query line 78
  14. instance OAI.MaxCutGames.Reduction.ActualGame.mapFintype line 80
  15. instance OAI.MaxCutGames.Reduction.ActualGame.dualFintype line 84
  16. def OAI.MaxCutGames.Reduction.ActualGame.canonical line 88
  17. abbrev OAI.MaxCutGames.Reduction.ActualGame.Vertex line 91
  18. abbrev OAI.MaxCutGames.Reduction.ActualGame.TwoSidedVertex line 92
  19. def OAI.MaxCutGames.Reduction.ActualGame.vertex line 94
  20. def OAI.MaxCutGames.Reduction.ActualGame.offset line 97
  21. def OAI.MaxCutGames.Reduction.ActualGame.shiftQuery line 100
  22. theorem OAI.MaxCutGames.Reduction.ActualGame.canonical_shiftQuery line 104
  23. theorem OAI.MaxCutGames.Reduction.ActualGame.vertex_shiftQuery line 110
  24. theorem OAI.MaxCutGames.Reduction.ActualGame.offset_shiftQuery line 116
  25. def OAI.MaxCutGames.Reduction.ActualGame.vertexCount line 121
  26. def OAI.MaxCutGames.Reduction.ActualGame.vertexEncoding line 124
  27. theorem OAI.MaxCutGames.Reduction.ActualGame.vertexCount_eq_twice line 128
  28. abbrev OAI.MaxCutGames.Reduction.ActualGame.Outcome line 133

    Source documentation

    Each product element is a separate edge occurrence.

    abbrev Outcome (S : Source) (k : Nat) {s d : Nat} (g : SplitGadget s d) :=
…
  29. def OAI.MaxCutGames.Reduction.ActualGame.leftQuery line 136
  30. def OAI.MaxCutGames.Reduction.ActualGame.rightQuery line 139
  31. def OAI.MaxCutGames.Reduction.ActualGame.edge line 143
  32. theorem OAI.MaxCutGames.Reduction.ActualGame.edge_source_ne_target line 150
  33. def OAI.MaxCutGames.Reduction.ActualGame.outcomes line 158
  34. theorem OAI.MaxCutGames.Reduction.ActualGame.mem_outcomes line 161
  35. theorem OAI.MaxCutGames.Reduction.ActualGame.outcomes_nodup line 165
  36. theorem OAI.MaxCutGames.Reduction.ActualGame.outcomes_length line 168
  37. def OAI.MaxCutGames.Reduction.ActualGame.outputInstance line 172
  38. theorem OAI.MaxCutGames.Reduction.ActualGame.outputInstance_constraints_length line 184
  39. def OAI.MaxCutGames.Reduction.ActualGame.sideLabel line 189
  40. def OAI.MaxCutGames.Reduction.ActualGame.labelingOf line 194
  41. theorem OAI.MaxCutGames.Reduction.ActualGame.sideLabel_labelingOf line 200
  42. def OAI.MaxCutGames.Reduction.ActualGame.unfolded line 206
  43. theorem OAI.MaxCutGames.Reduction.ActualGame.unfolded_equivariant line 211
  44. theorem OAI.MaxCutGames.Reduction.ActualGame.edge_satisfied_iff line 221
  45. def OAI.MaxCutGames.Reduction.ActualGame.acceptanceProbability line 235
  46. theorem OAI.MaxCutGames.Reduction.ActualGame.acceptanceProbability_eq_test line 240
  47. theorem OAI.MaxCutGames.Reduction.ActualGame.countSatisfied_map_inline_ActualGame line 252
  48. theorem OAI.MaxCutGames.Reduction.ActualGame.countSatisfied_eq_sum line 260
  49. theorem OAI.MaxCutGames.Reduction.ActualGame.acceptanceProbability_eq_count line 269

    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.MaxCutGames.Reduction.ActualGame.vertexCount, OAI.MaxCutGames.Reduction.ActualGame.acceptanceProbability, OAI.MaxCutGames.Reduction.ActualGame.outputInstance

  50. def OAI.MaxCutGames.Reduction.ActualGame.orbitBodyDecidableEq line 281
  51. def OAI.MaxCutGames.Reduction.ActualGame.explicitBodies line 286
  52. def OAI.MaxCutGames.Reduction.ActualGame.explicitVertexCount line 291
  53. def OAI.MaxCutGames.Reduction.ActualGame.explicitVertexEncoding line 294
  54. def OAI.MaxCutGames.Reduction.ActualGame.semanticToExplicitVertices line 302
  55. theorem OAI.MaxCutGames.Reduction.ActualGame.semanticToExplicitVertices_apply line 306
  56. theorem OAI.MaxCutGames.Reduction.ActualGame.explicitVertexCount_eq line 312
  57. def OAI.MaxCutGames.Reduction.ActualGame.explicitEdge line 316
  58. theorem OAI.MaxCutGames.Reduction.ActualGame.explicitEdge_eq_rename line 323
  59. def OAI.MaxCutGames.Reduction.ActualGame.explicitOutcomes line 330
  60. theorem OAI.MaxCutGames.Reduction.ActualGame.explicitOutcomes_nodup line 334
  61. theorem OAI.MaxCutGames.Reduction.ActualGame.mem_explicitOutcomes line 339
  62. theorem OAI.MaxCutGames.Reduction.ActualGame.explicitOutcomes_perm_outcomes line 344
  63. def OAI.MaxCutGames.Reduction.ActualGame.outputInstanceWithEnumeration line 354

    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.MaxCutGames.Foundations.Target.Instance

  64. theorem OAI.MaxCutGames.Reduction.ActualGame.outputInstanceWithEnumeration_length line 367
  65. theorem OAI.MaxCutGames.Reduction.ActualGame.explicitConstraints_perm_renamed line 374
  66. theorem OAI.MaxCutGames.Reduction.ActualGame.completeAt_outputInstanceWithEnumeration_iff line 383
  67. theorem OAI.MaxCutGames.Reduction.ActualGame.soundAt_outputInstanceWithEnumeration_iff line 391