OAI/Combinatorics/Progressions/Dynamics/CurrentLayerBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.currentLayerConstructionBudget line 9
2. def OAI.Erdos3.currentLayerRemovalBudget line 11
3. theorem OAI.Erdos3.currentLayerConstructionBudget_nonneg line 15
4. theorem OAI.Erdos3.currentLayerRemovalBudget_nonneg line 18
5. theorem OAI.Erdos3.le_currentLayerConstructionBudget line 23
6. theorem OAI.Erdos3.current_layer_construction_budget_bounds line 26
7. theorem OAI.Erdos3.current_layer_coordinate_factor_bound line 50
8. theorem OAI.Erdos3.current_layer_removal_budget_bounds line 66
9. theorem OAI.Erdos3.exists_current_layer_uniform_budget line 138