OAI/Computability/VertexCover/PCP/PreprocessingTables.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.PCP.PreprocessingTables.BaseTable line 15
  2. def OAI.UniqueGames.Foundations.PCP.PreprocessingTables.degree line 17
  3. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTables.degree_eq line 19
  4. def OAI.UniqueGames.Foundations.PCP.PreprocessingTables.regularVertices line 24
  5. def OAI.UniqueGames.Foundations.PCP.PreprocessingTables.vertices line 25
  6. def OAI.UniqueGames.Foundations.PCP.PreprocessingTables.padded line 27
  7. def OAI.UniqueGames.Foundations.PCP.PreprocessingTables.overlayFamily line 32
  8. def OAI.UniqueGames.Foundations.PCP.PreprocessingTables.preprocess line 37
  9. def OAI.UniqueGames.Foundations.PCP.PreprocessingTables.output line 42
  10. def OAI.UniqueGames.Foundations.PCP.PreprocessingTables.graphTable line 45
  11. def OAI.UniqueGames.Foundations.PCP.PreprocessingTables.outputBits line 48
  12. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTables.regularVertices_ge_darts line 51
  13. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTables.regularVertices_le line 55
  14. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTables.vertices_positive line 58
  15. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTables.vertices_le_of_positive line 61
  16. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTables.vertices_eq_one_of_no_darts line 71
  17. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTables.vertices_le line 76
  18. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTables.darts_eq line 86
  19. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTables.darts_le line 89
  20. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTables.vertices_le_inputBits line 97
  21. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTables.darts_le_inputBits line 102