OAI/Combinatorics/Progressions/Dynamics/PreparedSourceSideBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.prepared_slice_length_fraction line 10
2. theorem OAI.Erdos3.prepared_source_cost_add_required line 18
3. theorem OAI.Erdos3.prepared_source_side_budget line 30
4. theorem OAI.Erdos3.prepared_source_side_budgets line 46