OAI/Combinatorics/Progressions/Dynamics/ReducedTwistedTranslationBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.PolynomialTranslationLie.exists_weightedTranslationBuffered_scalar_budget line 12
2. theorem OAI.Erdos3.PolynomialTranslationLie.exists_weightedTranslationBuffered_budget line 120
3. theorem OAI.Erdos3.PolynomialTranslationLie.twistedBufferedTranslation_log_bound line 156
4. theorem OAI.Erdos3.PolynomialTranslationLie.exists_weightedTwistedTranslation_budget line 198
5. theorem OAI.Erdos3.PolynomialTranslationLie.exists_weightedTranslationTwistedNiltest_budget line 227
6. theorem OAI.Erdos3.PolynomialTranslationLie.exists_majorRationalLift_detection_budget line 262
7. theorem OAI.Erdos3.PolynomialTranslationLie.exists_reducedTwistedTranslation_budget line 315