OAI/Computability/VertexCover/PCP/PreprocessingLevels.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.levelLoop line 10
  2. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.levelLoop_level_le line 16
  3. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.levelLoop_power line 27
  4. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.levelLoop_covers line 38
  5. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.levelLoop_le_of_covering_power line 53
  6. def OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.searchResult line 70
  7. def OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.boundedLevel line 73
  8. def OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.paddedSize line 75
  9. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.boundedLevel_zero line 77
  10. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.paddedSize_zero line 79
  11. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_input line 81
  12. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.paddedSize_power line 85
  13. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.le_paddedSize line 90
  14. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.boundedLevel_eq_level line 94
  15. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.paddedSize_eq_size line 104
  16. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_of_le_power line 108
  17. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.paddedSize_positive line 113
  18. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.paddedSize_bounds line 117
  19. def OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize line 122
  20. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_zero line 124
  21. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_of_pos line 126
  22. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_bounds line 130
  23. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.table_vertexCount_eq_paddedSize line 138
  24. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingLevels.family_row_count_at_size line 149