OAI/Computability/UniqueGames/PCP/Clone100.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Outer.Clone100.triples line 19
  2. theorem OAI.UniqueGamesTheorem.Outer.Clone100.triples_length line 21
  3. def OAI.UniqueGamesTheorem.Outer.Clone100.clone line 24
  4. theorem OAI.UniqueGamesTheorem.Outer.Clone100.clone_distinct line 27
  5. theorem OAI.UniqueGamesTheorem.Outer.Clone100.clone_lift line 35
  6. def OAI.UniqueGamesTheorem.Outer.Clone100.nameEquiv line 38
  7. def OAI.UniqueGamesTheorem.Outer.Clone100.equation line 40
  8. theorem OAI.UniqueGamesTheorem.Outer.Clone100.equation_distinct line 45
  9. def OAI.UniqueGamesTheorem.Outer.Clone100.equations line 54
  10. theorem OAI.UniqueGamesTheorem.Outer.Clone100.equations_length line 58
  11. theorem OAI.UniqueGamesTheorem.Outer.Clone100.equations_nonempty line 67
  12. def OAI.UniqueGamesTheorem.Outer.Clone100.clonedInput line 73
  13. def OAI.UniqueGamesTheorem.Outer.Clone100.clonedSource line 78
  14. theorem OAI.UniqueGamesTheorem.Outer.Clone100.clonedSource_distinct line 81
  15. def OAI.UniqueGamesTheorem.Outer.Clone100.lift line 97
  16. theorem OAI.UniqueGamesTheorem.Outer.Clone100.equation_lift line 100
  17. theorem OAI.UniqueGamesTheorem.Outer.Clone100.completeness_count line 104
  18. def OAI.UniqueGamesTheorem.Outer.Clone100.success line 117
  19. theorem OAI.UniqueGamesTheorem.Outer.Clone100.completeness line 120
  20. theorem OAI.UniqueGamesTheorem.Outer.Clone100.count_as_sum line 128
  21. def OAI.UniqueGamesTheorem.Outer.Clone100.majority line 134
  22. theorem OAI.UniqueGamesTheorem.Outer.Clone100.equation_count_le line 137
  23. theorem OAI.UniqueGamesTheorem.Outer.Clone100.soundness_count line 160
  24. theorem OAI.UniqueGamesTheorem.Outer.Clone100.soundness line 174
  25. theorem OAI.UniqueGamesTheorem.Outer.Clone100.soundness_four_fifths line 192
  26. theorem OAI.UniqueGamesTheorem.Outer.Clone100.clonedInput_bits_length_le line 201