OAI/Combinatorics/Progressions/Estimates/CyclicProgressionHom.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.sum_predParam_smul_add line 13
2. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.freimanStep line 30
3. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.freimanAffine line 35
4. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.freimanAffine_pred_add_step line 39
5. theorem OAI.Erdos3.BohrProgression.CyclicCenteredGAP.freimanAffine_eq line 45
6. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.centerParam line 97
7. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.eval_centerParam line 99
8. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.eval_mem_carrier line 102
9. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.coeff_injective line 105
10. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.coefficientBox line 113
11. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.mem_coefficientBox line 116
12. lemma OAI.Erdos3.BohrProgression.CyclicCenteredGAP.mem_coefficientBox_iff_abs_le line 120
13. def OAI.Erdos3.BohrProgression.CyclicCenteredGAP.freimanHom line 136
14. theorem OAI.Erdos3.BohrProgression.CyclicCenteredGAP.freimanHom_coeff line 142
15. theorem OAI.Erdos3.BohrProgression.CyclicCenteredGAP.freimanHom_injOn line 164
16. theorem OAI.Erdos3.BohrProgression.CyclicCenteredGAP.image_freimanHom line 176