OAI/Analysis/IrrationalRotation/Sampling/SeparatedCharacterFrequencies.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.SeparatedCharacterFrequencies.sum_ne_zero_of_prefix_domination line 12
2. theorem OAI.Invariant233.SeparatedCharacterFrequencies.prefix_domination_of_relative_gaps line 59
3. theorem OAI.Invariant233.SeparatedCharacterFrequencies.fourier_zsmul line 83
4. theorem OAI.Invariant233.SeparatedCharacterFrequencies.product_fourier_characters line 87
5. theorem OAI.Invariant233.SeparatedCharacterFrequencies.integral_fourier_eq_zero line 95
6. theorem OAI.Invariant233.SeparatedCharacterFrequencies.integral_product_fourier_eq_zero line 100
7. theorem OAI.Invariant233.SeparatedCharacterFrequencies.eventually_nonzero_frequency line 106
8. theorem OAI.Invariant233.SeparatedCharacterFrequencies.eventually_integral_product_fourier_eq_zero line 139