OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/NormOneAddLeExp.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.NonpretentiousEuler.norm_one_add_le_exp line 16
2. lemma OAI.OrdinaryCorrelations.NonpretentiousEuler.norm_one_add_div_le_exp line 31
3. def OAI.OrdinaryCorrelations.NonpretentiousEuler.twist line 44
4. lemma OAI.OrdinaryCorrelations.NonpretentiousEuler.twist_norm_le line 47
5. lemma OAI.OrdinaryCorrelations.NonpretentiousEuler.distanceSq_nonneg line 55
6. def OAI.OrdinaryCorrelations.NonpretentiousEuler.normalizedProduct line 63
7. lemma OAI.OrdinaryCorrelations.NonpretentiousEuler.prime_inv_sq_sum_le line 67
8. theorem OAI.OrdinaryCorrelations.NonpretentiousEuler.norm_normalizedProduct_le line 81
9. theorem OAI.OrdinaryCorrelations.NonpretentiousEuler.eventual_uniformEuler_small line 114
10. theorem OAI.OrdinaryCorrelations.NonpretentiousEuler.tendsto_normalizedProduct line 140