OAI/Computability/UniqueGames/PCP/AlphabetReductionLemmas.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

The explicit assignment tester applied to the encoded satisfying pairs of an actual finite edge predicate. The resulting soundness loss is independent of the alphabet size. Uniform padding of the finite sample space and assembly of the global incidence graph are separate constructions.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetReduction.LegalPair line 29
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetReduction.InputCoordinate line 32
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetReduction.pairEncoding line 34
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetReduction.edgeTesterReject line 38
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetReduction.rejected_edge_tester_bound line 42
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetReduction.honest_edge_tester line 58
  7. structure OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph line 77
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.head line 88
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.head_reverse line 90
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.edgeSatisfied line 94
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.edgeSatisfied_reverse line 97
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.Satisfiable line 103
  13. def OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.rejectedDarts line 106
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.rejectionCount line 109
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.mem_rejectedDarts line 112
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.rejectionCount_le line 117
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.rejected_exists_of_not_satisfiable line 121
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.rejectionCount_positive line 133
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.rejectionCounts line 157
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.rejectionCounts_nonempty line 161
  21. def OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.minimumRejections line 166
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.minimumRejections_le line 169
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.exists_minimizer line 174
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.le_minimumRejections_iff line 181
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.minimumRejections_le_card line 191
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.rejectionCount_eq_zero_iff line 198
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.minimumRejections_eq_zero_iff line 213
  28. def OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.gap line 223
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.gap_nonnegative line 226
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.gap_le_one line 229
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.gap_eq_zero_iff line 235
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.le_gap_iff line 242

    Source documentation

    A lower bound on the actual minimum is exactly the universal count bound.

    theorem le_gap_iff [Nonempty E] (G : ConstraintGraph V E A) (ε : ℝ) :
    ε ≤ G.gap ↔ ∀ labeling : V → A,
      ε * Fintype.card E ≤ (G.rejectionCount labeling : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph

  33. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.inverse_card_le_gap_of_unsatisfiable line 255
  34. def OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.reindex line 272

    Source documentation

    Explicit changes of vertex, dart, and label coordinates.

    def reindex (G : ConstraintGraph V E A) (vertices : V ≃ W) (darts : E ≃ D)
    (labels : A ≃ B) : ConstraintGraph W D B where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph

  35. def OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.labelingEquiv line 286
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.reindex_edgeSatisfied line 292
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.reindex_rejectionCount line 299
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.rejectionCounts_reindex line 323
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.minimumRejections_reindex line 340
  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.gap_reindex line 346
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph.satisfiable_reindex line 352
  42. structure OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle line 381

    Source documentation

    Graphs of different finite sizes inhabit one fixed type for iteration.

    structure Bundle (A : Type) where
…
  43. instance OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.instFintypeVertex line 395
  44. instance OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.instFintypeDart line 396
  45. instance OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqVertex line 397
  46. instance OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqDart line 398
  47. instance OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.instNonemptyDart line 399
  48. instance OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.instNonemptyVertex line 402

    Source documentation

    A dart supplies a vertex through the actual tail map.

    instance instNonemptyVertex (G : Bundle A) : Nonempty G.Vertex := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle

  49. def OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.ofGraph line 406
  50. def OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.size line 418
  51. def OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.Satisfiable line 420
  52. def OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.rejectionCount line 422
  53. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.size_positive line 425
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.dartCard_le_size line 428
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.ofGraph_graph line 431
  56. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.ofGraph_size line 435
  57. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.ofGraph_satisfiable line 439
  58. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.ofGraph_rejectionCount line 443
  59. def OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.minimumRejections line 452
  60. def OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.gap line 454
  61. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.exists_minimizer line 456
  62. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.gap_nonnegative line 460
  63. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.gap_le_one line 462
  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.gap_eq_zero_iff line 464
  65. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.le_gap_iff line 467
  66. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.inverse_card_le_gap_of_unsatisfiable line 472
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.one_le_dartCard_mul_gap line 476
  68. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.one_le_size_mul_gap line 483

    Source documentation

    The actual total graph size supplies the initial inverse-size gap.

    theorem one_le_size_mul_gap (G : Bundle A) (unsat : ¬ G.Satisfiable) :
    1 ≤ (G.size : ℝ) * G.gap := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle

  69. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.ofGraph_minimumRejections line 490
  70. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FiniteGraph.Bundle.ofGraph_gap line 494