OAI/Computability/UniqueGames/Games/FinishBoundsLemmas.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Scalar estimates for the construction. These lemmas only perform the stated rounding/subdivision/repetition arithmetic; they do not assume or assert an unproved repetition theorem or hardness result.

  1. theorem OAI.UniqueGamesTheorem.Explicit.FinishBounds.exists_reciprocal_tolerance line 29
  2. theorem OAI.UniqueGamesTheorem.Explicit.FinishBounds.subdivision_completeness line 48
  3. theorem OAI.UniqueGamesTheorem.Explicit.FinishBounds.subdivision_soundness line 55
  4. theorem OAI.UniqueGamesTheorem.Explicit.FinishBounds.final_completeness line 63

    Source documentation

    The full completeness loss after the coordinatewise product labeling.

    theorem final_completeness (vB vG d τ ε₀ ε : ℝ) (t : Nat) (ht : 0 < t)
    (hB : 1 - (d + τ) / 4 ≤ vB)
    (hG : 1 - (t : ℝ) * (1 - vB) ≤ vG)
    (hd : d ≤ ε₀ / t) (hτ : τ ≤ ε₀ / t)
    (hε₀ : 0 ≤ ε₀) (hε : ε₀ ≤ ε) :
    1 - ε ≤ vG := by
…
  5. structure OAI.UniqueGamesTheorem.Explicit.OccurrenceGame line 92
  6. structure OAI.UniqueGamesTheorem.Explicit.BipartiteGame line 97
  7. def OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.Satisfied line 105
  8. instance OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.satisfiedDecidable line 109
  9. def OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.IsTranslation line 113
  10. def OAI.UniqueGamesTheorem.Explicit.BipartiteGame.Satisfied line 120
  11. instance OAI.UniqueGamesTheorem.Explicit.BipartiteGame.satisfiedDecidable line 124
  12. def OAI.UniqueGamesTheorem.Explicit.BipartiteGame.IsTranslation line 128
  13. def OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.satisfiedCount line 154
  14. theorem OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.satisfiedCount_eq_sum_satisfied line 157
  15. def OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.maxSatisfied line 172
  16. def OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.value line 176
  17. theorem OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.satisfiedCount_le_maxSatisfied line 179
  18. theorem OAI.UniqueGamesTheorem.Explicit.OccurrenceGame.maxSatisfied_attained line 184
  19. def OAI.UniqueGamesTheorem.Explicit.BipartiteGame.satisfiedCount line 197
  20. theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.satisfiedCount_eq_sum_satisfied line 200
  21. def OAI.UniqueGamesTheorem.Explicit.BipartiteGame.maxSatisfied line 216
  22. def OAI.UniqueGamesTheorem.Explicit.BipartiteGame.value line 220
  23. theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.satisfiedCount_le_maxSatisfied line 223
  24. theorem OAI.UniqueGamesTheorem.Explicit.BipartiteGame.maxSatisfied_attained line 229
  25. abbrev OAI.UniqueGamesTheorem.Explicit.Subdivision.Left line 244

    Source documentation

    Original vertices and the middle vertices q_e.

    abbrev Left (V E : Type*) := V ⊕ E
  26. abbrev OAI.UniqueGamesTheorem.Explicit.Subdivision.Right line 247

    Source documentation

    false is p_e, and true is r_e.

    abbrev Right (E : Type*) := E × Bool
  27. abbrev OAI.UniqueGamesTheorem.Explicit.Subdivision.Edge line 249
  28. def OAI.UniqueGamesTheorem.Explicit.Subdivision.left line 251
  29. def OAI.UniqueGamesTheorem.Explicit.Subdivision.right line 256
  30. def OAI.UniqueGamesTheorem.Explicit.Subdivision.permutation line 258
  31. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.endpoints_injective line 263

    Source documentation

    The private occurrence identifier prevents parallel edges after subdivision. This also handles a loop, which becomes a genuine four-cycle.

    theorem endpoints_injective (g : OccurrenceGame V E A) :
    Function.Injective (fun ei : Edge E => (left g ei, right ei)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.OccurrenceGame, OAI.UniqueGamesTheorem.Explicit.Subdivision.Edge, OAI.UniqueGamesTheorem.Explicit.Subdivision.left, OAI.UniqueGamesTheorem.Explicit.Subdivision.right

  32. def OAI.UniqueGamesTheorem.Explicit.Subdivision.game line 270
  33. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.isTranslation line 278

    Source documentation

    Reversing the last edge negates its translation offset.

    theorem isTranslation [AddGroup A] (g : OccurrenceGame V E A)
    (hg : g.IsTranslation) : (game g).IsTranslation := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.OccurrenceGame, OAI.UniqueGamesTheorem.Explicit.Subdivision.game

  34. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.binary_translation_offsets line 291

    Source documentation

    In a binary additive alphabet the inverse offset is the original offset.

    theorem binary_translation_offsets [AddGroup A]
    (hbinary : ∀ a : A, a + a = 0) (g : OccurrenceGame V E A)
    (c : E → A) (hc : ∀ e a, g.permutation e a = a + c e) :
    ∀ ei a, (game g).permutation ei a =
      a + (if ei.2 = 3 then c ei.1 else 0) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.OccurrenceGame, OAI.UniqueGamesTheorem.Explicit.Subdivision.game, OAI.UniqueGamesTheorem.Explicit.Subdivision.permutation

  35. def OAI.UniqueGamesTheorem.Explicit.Subdivision.restrict line 304

    Source documentation

    Restrict any output labeling to the original vertices.

    def restrict (a : Left V E → A) : V → A := fun v => a (Sum.inl v)

    Mentions: OAI.UniqueGamesTheorem.Explicit.Subdivision.Left

  36. def OAI.UniqueGamesTheorem.Explicit.Subdivision.extendLeft line 306
  37. def OAI.UniqueGamesTheorem.Explicit.Subdivision.extendRight line 309
  38. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.restrict_extendLeft line 312
  39. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.four_satisfied_implies_original line 316

    Source documentation

    All four equations along the path force the original permutation equation.

    theorem four_satisfied_implies_original (ρ : Equiv.Perm A) (u p q r v : A)
    (h₀ : u = p) (h₁ : q = p) (h₂ : q = r) (h₃ : ρ.symm v = r) :
    ρ u = v := by
…
  40. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.local_count_le line 326

    Source documentation

    The strongest possible path score for fixed endpoint labels is exactly three plus the old satisfaction indicator.

    theorem local_count_le (ρ : Equiv.Perm A) (u p q r v : A) :
    (if u = p then 1 else 0) + (if q = p then 1 else 0) +
      (if q = r then 1 else 0) + (if ρ.symm v = r then 1 else 0) ≤
        3 + (if ρ u = v then 1 else 0 : Nat) := by
…
  41. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.local_count_extend line 334
  42. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.count_on_occurrence_le line 347
  43. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.count_on_occurrence_extend line 358
  44. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.satisfiedCount_le line 369
  45. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.satisfiedCount_extend line 382

    Source documentation

    Fresh interiors can be assigned independently, so the upper bound is attained.

    theorem satisfiedCount_extend (g : OccurrenceGame V E A) (a : V → A) :
    (game g).satisfiedCount (extendLeft g a) (extendRight g a) =
      3 * Fintype.card E + g.satisfiedCount a := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.OccurrenceGame, OAI.UniqueGamesTheorem.Explicit.Subdivision.game, OAI.UniqueGamesTheorem.Explicit.Subdivision.extendLeft, OAI.UniqueGamesTheorem.Explicit.Subdivision.extendRight

  46. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.edge_count line 390
  47. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.left_count line 393
  48. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.right_count line 397
  49. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.maxSatisfied_eq line 402
  50. theorem OAI.UniqueGamesTheorem.Explicit.Subdivision.value_eq line 414
  51. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.weight_eq_probability_singleton line 437
  52. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.pushforward_comp line 442
  53. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.transport_eq_pushforward line 450
  54. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.expectation_pushforward line 458
  55. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.pushforward_mixture line 467