OAI/Computability/UniqueGames/PCP/Clone100Triples.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The concrete clone sample space. Global distinctness is a stronger conditioning rule than distinctness only at repeated original variables. It retains the same 3/100 bound and makes the number of copies uniform.

  1. abbrev OAI.UniqueGamesTheorem.Outer.Clone100Triples.Index line 16
  2. abbrev OAI.UniqueGamesTheorem.Outer.Clone100Triples.Triple line 17
  3. def OAI.UniqueGamesTheorem.Outer.Clone100Triples.good line 19
  4. instance OAI.UniqueGamesTheorem.Outer.Clone100Triples.(instance at line 22) line 22
  5. abbrev OAI.UniqueGamesTheorem.Outer.Clone100Triples.GoodTriple line 24
  6. def OAI.UniqueGamesTheorem.Outer.Clone100Triples.toEmbedding line 26
  7. def OAI.UniqueGamesTheorem.Outer.Clone100Triples.fromEmbedding line 35
  8. def OAI.UniqueGamesTheorem.Outer.Clone100Triples.embeddingEquiv line 43
  9. theorem OAI.UniqueGamesTheorem.Outer.Clone100Triples.card_goodTriple line 53
  10. theorem OAI.UniqueGamesTheorem.Outer.Clone100Triples.card_triple line 57
  11. instance OAI.UniqueGamesTheorem.Outer.Clone100Triples.(instance at line 60) line 60