OAI/Computability/VertexCover/PCP/RoundTables.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.PCP.RoundTables.BaseTable line 14
  2. opaque OAI.UniqueGames.Foundations.PCP.RoundTables.fixedWalkParameter line 16
  3. def OAI.UniqueGames.Foundations.PCP.RoundTables.walkParameter line 19
  4. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.walkParameter_eq line 21
  5. def OAI.UniqueGames.Foundations.PCP.RoundTables.alphabet line 24
  6. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.alphabet_positive line 26
  7. def OAI.UniqueGames.Foundations.PCP.RoundTables.powered line 30
  8. def OAI.UniqueGames.Foundations.PCP.RoundTables.build line 33
  9. def OAI.UniqueGames.Foundations.PCP.RoundTables.sizeFactor line 36
  10. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.degree_positive line 39
  11. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.dartFactor_positive line 43
  12. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.sizeFactor_positive line 47
  13. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.powered_vertices line 54
  14. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.powered_darts line 57
  15. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.build_darts_positive line 61
  16. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.build_size_le line 69
  17. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.build_completeness line 96
  18. abbrev OAI.UniqueGames.Foundations.PCP.RoundTables.Input line 105
  19. instance OAI.UniqueGames.Foundations.PCP.RoundTables.(instance at line 107) line 107
  20. def OAI.UniqueGames.Foundations.PCP.RoundTables.step line 109
  21. def OAI.UniqueGames.Foundations.PCP.RoundTables.initial line 112
  22. def OAI.UniqueGames.Foundations.PCP.RoundTables.size line 115
  23. def OAI.UniqueGames.Foundations.PCP.RoundTables.Satisfiable line 117
  24. def OAI.UniqueGames.Foundations.PCP.RoundTables.gap line 119
  25. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.size_positive line 121
  26. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.gap_nonnegative line 124
  27. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.gap_eq_zero_iff line 127
  28. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.one_le_size_mul_gap line 130
  29. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.initial_satisfiable_iff line 142
  30. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.step_completeness line 145
  31. theorem OAI.UniqueGames.Foundations.PCP.RoundTables.step_size line 148