OAI/Computability/VertexCover/PCP/InitialGraph.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.PCP.InitialGraph.Label line 13
  2. abbrev OAI.UniqueGames.Foundations.PCP.InitialGraph.Vertex line 14
  3. abbrev OAI.UniqueGames.Foundations.PCP.InitialGraph.Dart line 15
  4. instance OAI.UniqueGames.Foundations.PCP.InitialGraph.slotFintype line 17
  5. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.card_slot line 21
  6. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.card_label line 22
  7. def OAI.UniqueGames.Foundations.PCP.InitialGraph.variableVertex line 25
  8. def OAI.UniqueGames.Foundations.PCP.InitialGraph.clauseVertex line 26
  9. def OAI.UniqueGames.Foundations.PCP.InitialGraph.dummyVertex line 27
  10. def OAI.UniqueGames.Foundations.PCP.InitialGraph.dummyDart line 28
  11. instance OAI.UniqueGames.Foundations.PCP.InitialGraph.vertexNonempty line 30
  12. instance OAI.UniqueGames.Foundations.PCP.InitialGraph.dartNonempty line 31
  13. def OAI.UniqueGames.Foundations.PCP.InitialGraph.reverse line 33
  14. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.reverse_involutive line 37
  15. def OAI.UniqueGames.Foundations.PCP.InitialGraph.reverseEquiv line 43
  16. def OAI.UniqueGames.Foundations.PCP.InitialGraph.tail line 49
  17. def OAI.UniqueGames.Foundations.PCP.InitialGraph.toClauseAnswer line 54
  18. def OAI.UniqueGames.Foundations.PCP.InitialGraph.fromClauseAnswer line 55
  19. def OAI.UniqueGames.Foundations.PCP.InitialGraph.variableLabel line 56
  20. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.to_fromClauseAnswer line 58
  21. def OAI.UniqueGames.Foundations.PCP.InitialGraph.variableValid line 62
  22. def OAI.UniqueGames.Foundations.PCP.InitialGraph.incidenceAccept line 65
  23. def OAI.UniqueGames.Foundations.PCP.InitialGraph.predicate line 71
  24. def OAI.UniqueGames.Foundations.PCP.InitialGraph.raw line 76
  25. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.raw_forward line 87
  26. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.incidenceAccept_true line 92
  27. def OAI.UniqueGames.Foundations.PCP.InitialGraph.honestLabeling line 99
  28. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.incidence_honest line 104
  29. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.raw_completeness line 112
  30. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.clauseAnswer_eq_of_slots line 121
  31. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.raw_reflects line 130
  32. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.raw_satisfiable_iff line 149
  33. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.card_vertex line 152
  34. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.card_dart line 156
  35. abbrev OAI.UniqueGames.Foundations.PCP.InitialGraph.CompactVertex line 161
  36. abbrev OAI.UniqueGames.Foundations.PCP.InitialGraph.CompactDart line 162
  37. def OAI.UniqueGames.Foundations.PCP.InitialGraph.build line 164
  38. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.build_satisfiable_iff line 167
  39. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.build_vertex_bound line 171
  40. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.build_dart_count line 177
  41. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.build_initial_gap line 181
  42. theorem OAI.UniqueGames.Foundations.PCP.InitialGraph.build_inverse_size_gap line 187