OAI/Combinatorics/Progressions/Estimates/NormalizedCutoffs.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.abs_div_sub_div_bound line 14
2. def OAI.Erdos3.normalizedCutoffs line 45
3. theorem OAI.Erdos3.cutoffCover_sum_ge_one line 48
4. theorem OAI.Erdos3.normalizedCutoffs_range line 54
5. theorem OAI.Erdos3.sum_normalizedCutoffs line 62
6. theorem OAI.Erdos3.tsupport_normalizedCutoffs_subset line 67
7. theorem OAI.Erdos3.lipschitz_normalizedCutoffs line 73
8. theorem OAI.Erdos3.contMDiff_normalizedCutoffs_comp line 97