OAI/Combinatorics/Progressions/Results/Reciprocal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.reciprocalTerm_nonneg line 11
2. theorem OAI.Erdos3.reciprocalTerm_zero line 16
3. theorem OAI.Erdos3.dyadic_sum_le line 20
4. theorem OAI.Erdos3.reciprocal_sum_le_dyadic_tsum line 43
5. theorem OAI.Erdos3.summable_reciprocal_of_APFree line 66
6. theorem OAI.Erdos3.hasAP_of_not_summable_reciprocal line 86