OAI/Combinatorics/Progressions/Estimates/LinearCutoff.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.linearCutoff line 12
2. theorem OAI.Erdos3.linearCutoff_range line 15
3. theorem OAI.Erdos3.linearCutoff_eq_one line 19
4. theorem OAI.Erdos3.linearCutoff_eq_zero line 25
5. theorem OAI.Erdos3.linearCutoff_mono_center line 31
6. theorem OAI.Erdos3.linearCutoff_lipschitz line 37