OAI/Combinatorics/Progressions/Dynamics/AdaptedMapGeometryBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.adaptedMapGeometryBudget line 10
2. theorem OAI.Erdos3.adaptedMapGeometryBudget_nonneg line 13
3. theorem OAI.Erdos3.adaptedMapGeometryBudget_geometry line 18
4. theorem OAI.Erdos3.adaptedMapGeometryBudget_inverse line 27
5. theorem OAI.Erdos3.adaptedMapGeometryBudget_markedMap line 36
6. theorem OAI.Erdos3.adaptedMapGeometryBudget_parameter line 43
7. theorem OAI.Erdos3.exists_adaptedMapGeometryBudget_fixed_power line 53