OAI/NumberTheory/OrdinaryCorrelations/Elliott/Cesaro.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.ElliottReductions.cesaro line 33
2. lemma OAI.OrdinaryCorrelations.ElliottReductions.cesaro_translation_bound line 36
3. theorem OAI.OrdinaryCorrelations.ElliottReductions.cesaro_translation_error line 45
4. lemma OAI.OrdinaryCorrelations.ElliottReductions.cesaro_translation_tendsto line 55
5. lemma OAI.OrdinaryCorrelations.ElliottReductions.shiftAverage_swap line 60
6. lemma OAI.OrdinaryCorrelations.ElliottReductions.shiftAverage_translate line 68
7. lemma OAI.OrdinaryCorrelations.ElliottReductions.shiftAverage_of_anchored line 85
8. lemma OAI.OrdinaryCorrelations.ElliottReductions.shiftAverage_zero_left line 92
9. lemma OAI.OrdinaryCorrelations.ElliottReductions.shiftAverage_zero_right line 101
10. theorem OAI.OrdinaryCorrelations.ElliottReductions.cancellation_of_value_one_zero line 106