OAI/Combinatorics/Progressions/Estimates/LocalShiftFiber.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos3.CyclicCrootSisask.bigShifts_step_one line 26
2. lemma OAI.Erdos3.CyclicCrootSisask.reindex_shift_count line 36
3. lemma OAI.Erdos3.CyclicCrootSisask.bigShifts_step_two line 55
4. theorem OAI.Erdos3.CyclicCrootSisask.bigShifts line 112
5. def OAI.Erdos3.CyclicCrootSisask.setAverageTranslate line 149
6. def OAI.Erdos3.CyclicCrootSisask.centeredTranslate line 153
7. def OAI.Erdos3.CyclicCrootSisask.sampleDeviation line 157
8. lemma OAI.Erdos3.CyclicCrootSisask.sum_centeredTranslate_eq_zero line 163
9. theorem OAI.Erdos3.CyclicCrootSisask.pointwise_sampleDeviation_moment line 175
10. theorem OAI.Erdos3.CyclicCrootSisask.global_sampleDeviation_moment line 193
11. lemma OAI.Erdos3.CyclicCrootSisask.abs_setAverageTranslate_le line 216
12. lemma OAI.Erdos3.CyclicCrootSisask.abs_centeredTranslate_le line 239
13. theorem OAI.Erdos3.CyclicCrootSisask.global_sampleDeviation_moment_of_bounded line 251
14. lemma OAI.Erdos3.CyclicCrootSisask.markov_card_good line 278
15. def OAI.Erdos3.CyclicCrootSisask.goodSamples line 295
16. lemma OAI.Erdos3.CyclicCrootSisask.mem_goodSamples line 301
17. theorem OAI.Erdos3.CyclicCrootSisask.half_samples_are_good line 309
18. lemma OAI.Erdos3.CyclicCrootSisask.sampleDeviation_sub_const_identity line 348
19. theorem OAI.Erdos3.CyclicCrootSisask.goodSamples_give_almost_period line 363
20. theorem OAI.Erdos3.CyclicCrootSisask.exists_large_almostPeriod_set line 424
21. lemma OAI.Erdos3.CyclicCrootSisask.card_shiftSet_lower_bound line 489
22. theorem OAI.Erdos3.CyclicCrootSisask.exists_many_almostPeriods_of_smallDoubling line 529
23. theorem OAI.Erdos3.CyclicCrootSisask.exists_local_shift_fiber line 566