OAI/Combinatorics/IndependentSets/Expansion/PreprocessingRegularBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.offset_succ line 14
2. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.blocksPrefix_length_le line 22
3. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.header line 28
4. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.ownerBits line 31
5. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.originalPrefix line 36
6. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix line 41
7. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix line 47
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.originalPrefix_length_le line 55
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix_length_le line 63
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix_length_le line 74
11. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.regular_originalPrefix_le line 88
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.regular_ownerPrefix_le line 95
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.regular_dummyPrefix_le line 102
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.visits_le_input line 109
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularBounds.sum_body_costs_le line 119