OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/MovingParameters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.PretentiousEuler.MovingParameters line 25
2. def OAI.OrdinaryCorrelations.PretentiousEuler.movingFilter line 26
3. lemma OAI.OrdinaryCorrelations.PretentiousEuler.moving_length_tendsto line 28
4. lemma OAI.OrdinaryCorrelations.PretentiousEuler.quotient_square_dominates line 31
5. lemma OAI.OrdinaryCorrelations.PretentiousEuler.normalized_sum_small line 38
6. lemma OAI.OrdinaryCorrelations.PretentiousEuler.moving_quotient_mean_tendsto line 46
7. lemma OAI.OrdinaryCorrelations.PretentiousEuler.moving_normalized_div_tendsto line 67
8. theorem OAI.OrdinaryCorrelations.PretentiousEuler.moving_multiplicative_mean_tendsto_zero line 88