OAI/Combinatorics/Progressions/Nilpotent/BracketStepBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.bracketConstructionBudget line 9
2. def OAI.Erdos3.bracketCorrectionBudget line 11
3. theorem OAI.Erdos3.bracketConstructionBudget_nonneg line 15
4. theorem OAI.Erdos3.bracketCorrectionBudget_nonneg line 18
5. theorem OAI.Erdos3.bracket_construction_budget_bounds line 24
6. theorem OAI.Erdos3.bracket_correction_budget_bounds line 38
7. theorem OAI.Erdos3.exists_bracket_uniform_budget line 67