OAI/Combinatorics/Progressions/Dynamics/CoefficientScaleLogBudget.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.coefficientRowAccuracy_inverse_le_expline 9 - def
OAI.Erdos3.coefficientToleranceLogline 19 - theorem
OAI.Erdos3.coefficientToleranceLog_nonnegline 23 - theorem
OAI.Erdos3.coefficientToleranceScale_le_expline 30