OAI/Combinatorics/Progressions/Fourier/RationalLiftCharacterTwist.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.real_fourierChar_norm_sub_le line 13
2. theorem OAI.Erdos3.real_fourierChar_norm_sub_le_four_mul line 31
3. def OAI.Erdos3.rationalLiftCharacterTwist line 49
4. def OAI.Erdos3.rationalLiftCharacterTwistLip line 53
5. theorem OAI.Erdos3.rationalLiftCharacterTwist_norm line 56
6. theorem OAI.Erdos3.rationalLiftCharacterTwist_lipschitz line 60
7. theorem OAI.Erdos3.rationalLiftCharacterTwistLip_le line 94
8. theorem OAI.Erdos3.rationalLiftCharacterTwist_residual line 107