OAI/Combinatorics/Progressions/FixedDensity/ShortInterval.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.FixedDensity.cyclicAPVal line 10
2. theorem OAI.Erdos3.FixedDensity.cyclicAPVal_cast line 14
3. theorem OAI.Erdos3.FixedDensity.abs_secondDifference_le line 19
4. theorem OAI.Erdos3.FixedDensity.cyclicAPVal_secondDifference_eq_zero line 27
5. theorem OAI.Erdos3.FixedDensity.eq_affine_of_secondDifference_zero line 54
6. theorem OAI.Erdos3.FixedDensity.cyclicAPVal_eq_affine line 78
7. theorem OAI.Erdos3.FixedDensity.cyclicAPVal_one_sub_zero_ne_zero line 93
8. theorem OAI.Erdos3.FixedDensity.cyclicAPVal_isIntegerAP line 106