OAI/Combinatorics/IndependentSets/Expansion/PreprocessingLevels.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.levelLoop line 8
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.levelLoop_level_le line 14
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.levelLoop_power line 25
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.levelLoop_covers line 36
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.levelLoop_le_of_covering_power line 51
  6. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.searchResult line 68
  7. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.boundedLevel line 71
  8. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.paddedSize line 73
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.boundedLevel_zero line 75
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.paddedSize_zero line 77
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_input line 79
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.paddedSize_power line 83
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.le_paddedSize line 88
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.boundedLevel_eq_level line 92
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.paddedSize_eq_size line 102
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_of_le_power line 106
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.paddedSize_positive line 111
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.paddedSize_bounds line 115
  19. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize line 120
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_zero line 122
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_of_pos line 124
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_bounds line 128
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.table_vertexCount_eq_paddedSize line 136
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingLevels.family_row_count_at_size line 147