OAI/Combinatorics/Progressions/Fourier/FiniteSpectrumCutoff.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.spectrumTail line 11
2. theorem OAI.Erdos3.spectrumTail_le_card line 14
3. theorem OAI.Erdos3.spectrumTail_step line 26
4. theorem OAI.Erdos3.spectrumTail_levels line 44
5. theorem OAI.Erdos3.spectrumTail_geometric line 61
6. theorem OAI.Erdos3.finite_series_truncation_le line 84
7. theorem OAI.Erdos3.finite_series_norm_le line 106
8. theorem OAI.Erdos3.spectrumTail_finite_levels line 124
9. theorem OAI.Erdos3.spectrumTail_finite_geometric line 140