OAI/Computability/UniqueGames/PCP/CodeComposition.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.disagreement line 15
  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.disagreement_self line 17
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.disagreement_nonnegative line 20
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.disagreement_le_one line 23
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.disagreement_comm line 26
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.disagreement_triangle line 29
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.disagreement_eq_sign line 33
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.relativeDistance line 37
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.relativeDistance_self line 40
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.relativeDistance_nonnegative line 44
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.relativeDistance_comm line 48
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.relativeDistance_triangle line 52
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.relativeDistance_eq_sign line 58
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.codeword line 66

    Source documentation

    The encoding is a literal coordinate read from a finite Boolean truth table.

    def codeword {A : Type*} (a : A) : Cube A → Bool := fun x => x a
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.singletonMask line 68
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.walsh_singletonMask line 71
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.singletonMask_ne line 81
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.codeword_distance line 87
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.exists_nearest line 98
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.nearest line 107

    Source documentation

    Classical choice is used only for the soundness analysis, not the output algorithm.

    def nearest {A : Type*} [Fintype A] [DecidableEq A] [Nonempty A] (f : Cube A → Bool) : A :=
…
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.nearest_minimal line 110
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.distance_from_other_codeword line 115
  23. def OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.pairWord line 124

    Source documentation

    Two equal-sized blocks, indexed by a side bit and a common coordinate.

    def pairWord {X : Type*} (left right : X → Bool) : Bool × X → Bool :=
…
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.pairWord_distance line 127
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.rejected_pair_far line 137

    Source documentation

    Every satisfying encoded pair is far from a pair whose nearest decoding rejects.

    theorem rejected_pair_far {A : Type*} [Fintype A] [DecidableEq A] [Nonempty A]
    (accepts : A → A → Bool) (left right : Cube A → Bool)
    (hbad : accepts (nearest left) (nearest right) = false)
    (a b : A) (hgood : accepts a b = true) :
    1 / 8 ≤ relativeDistance (pairWord left right)
      (pairWord (codeword a) (codeword b)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.accepts, OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.nearest, OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.relativeDistance, OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.pairWord, OAI.UniqueGamesTheorem.Foundations.PCP.CodeComposition.codeword