OAI/Combinatorics/Progressions/Geometry/QuotientCoordinateRadius.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.quotientCoordinateRadius line 9
2. theorem OAI.Erdos3.quotientCoordinateRadius_pos line 12
3. theorem OAI.Erdos3.quotientCoordinateRadius_le_one line 17
4. theorem OAI.Erdos3.quotientCoordinateRadius_small line 24
5. theorem OAI.Erdos3.quotientCoordinateRadius_inverse line 31
6. theorem OAI.Erdos3.quotientCoordinateRadius_inverse_power_budget line 36
7. theorem OAI.Erdos3.product_two_power_bounds line 84
8. theorem OAI.Erdos3.quotient_chart_parameter_budget line 95