OAI/Combinatorics/Progressions/Estimates/WeightedTwistedTranslationLipschitz.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.PolynomialTranslationLie.translationDisplacementNN line 20
2. def OAI.Erdos3.PolynomialTranslationLie.bufferedTranslationTermLip line 24
3. theorem OAI.Erdos3.PolynomialTranslationLie.bufferedTranslationTerm_lipschitz line 28
4. theorem OAI.Erdos3.PolynomialTranslationLie.bufferedTranslationPhase_lipschitz line 84
5. theorem OAI.Erdos3.complex_mul_sub_mul_le_unit line 109
6. def OAI.Erdos3.PolynomialTranslationLie.twistedBufferedTranslationTermLip line 131
7. theorem OAI.Erdos3.PolynomialTranslationLie.twistedBufferedTranslationTerm_lipschitz line 135
8. theorem OAI.Erdos3.PolynomialTranslationLie.twistedBufferedTranslationPhase_lipschitz line 206