OAI/Combinatorics/Progressions/Estimates/InactiveAxisScale.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.inactiveSideLength line 10
2. def OAI.Erdos3.inactivePrincipalCoefficient line 13
3. theorem OAI.Erdos3.inactiveSideLength_pos line 15
4. theorem OAI.Erdos3.inactiveSideLength_power line 24
5. theorem OAI.Erdos3.inactiveSideLength_le line 28
6. theorem OAI.Erdos3.inactiveSideLength_lower_power line 35
7. theorem OAI.Erdos3.inactivePrincipal_small line 51
8. theorem OAI.Erdos3.inactivePrincipal_large line 55