OAI/Combinatorics/Progressions/Fourier/WeightedTranslationTwistedCentralFrequency.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_vertical_decomposition_preserving_bounds_and_characters line 19
2. theorem OAI.Erdos3.exists_native_vertical_pair_preserving_characters_on_finset line 71
3. theorem OAI.Erdos3.exists_native_vertical_pair_preserving_characters_power line 148
4. theorem OAI.Erdos3.PolynomialTranslationLie.central_character_eq_fourierChar line 209
5. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslation_frequency_one_of_central line 216
6. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslation_selected_frequency_one line 238
7. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationTwistedObservable_central line 278
8. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslation_twisted_selected_frequency_one line 294