OAI/Combinatorics/Progressions/Geometry/NormalizedSupportPlateau.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.normalizedSupportPlateau line 14
2. theorem OAI.Erdos3.normalizedSupportPlateau_range line 17
3. theorem OAI.Erdos3.normalizedSupportPlateau_one line 21
4. theorem OAI.Erdos3.normalizedSupportPlateau_support line 26
5. theorem OAI.Erdos3.normalizedSupportPlateau_lipschitz line 37
6. theorem OAI.Erdos3.normalizedSupportPlateau_grid_one line 46
7. theorem OAI.Erdos3.normalizedSupportPlateau_grid_support line 54