OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/RealPowerHom.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.PretentiousEuler.realPowerHom line 18
2. def OAI.OrdinaryCorrelations.PretentiousEuler.weightedHom line 24
3. lemma OAI.OrdinaryCorrelations.PretentiousEuler.weightedHom_norm_summable line 34
4. lemma OAI.OrdinaryCorrelations.PretentiousEuler.realPowerHom_norm_summable line 43
5. lemma OAI.OrdinaryCorrelations.PretentiousEuler.negativePower_le_inv line 49
6. lemma OAI.OrdinaryCorrelations.PretentiousEuler.prime_weight_half line 54
7. lemma OAI.OrdinaryCorrelations.PretentiousEuler.prime_weight_squares_le line 59
8. lemma OAI.OrdinaryCorrelations.PretentiousEuler.cutoff_negativePower_lower line 76
9. lemma OAI.OrdinaryCorrelations.PretentiousEuler.realPower_euler_tendsto line 93
10. lemma OAI.OrdinaryCorrelations.PretentiousEuler.weighted_euler_tendsto line 99