OAI/NumberTheory/Jacobsthal/Paths/TagCutoffSeparation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosStoppedTagSieve.interval_AP_li_error line 13
2. theorem OAI.Erdos970.ErdosStoppedTagSieve.interval_AP_count_error line 60
3. lemma OAI.Erdos970.ErdosStoppedTagSieve.moving_lower_ge_self line 101
4. lemma OAI.Erdos970.ErdosStoppedTagSieve.cubeHeight_moving_lower line 110
5. theorem OAI.Erdos970.ErdosStoppedTagSieve.eventually_moving_exponential_domination line 126
6. theorem OAI.Erdos970.ErdosStoppedTagSieve.eventually_moving_error line 166
7. lemma OAI.Erdos970.ErdosStoppedTagSieve.eventually_cutoff_dominates line 215
8. lemma OAI.Erdos970.ErdosStoppedTagSieve.eventually_cutoff_le_subbin line 236