OAI/NumberTheory/DirichletL/Moments/FirstDivisorCommonBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFirstDivisorCommonBound.pairMajorant line 23
2. lemma OAI.SevenEighths.CenteredMomentFirstDivisorCommonBound.pairMajorant_nonneg line 28
3. lemma OAI.SevenEighths.CenteredMomentFirstDivisorCommonBound.gaussEnergy_pair_bound line 34
4. def OAI.SevenEighths.CenteredMomentFirstDivisorCommonBound.coarse line 53
5. lemma OAI.SevenEighths.CenteredMomentFirstDivisorCommonBound.coarse_nonneg line 59
6. lemma OAI.SevenEighths.CenteredMomentFirstDivisorCommonBound.commonEnergy_coarse line 63
7. theorem OAI.SevenEighths.CenteredMomentFirstDivisorCommonBound.actual_supported_annular_block line 75
8. theorem OAI.SevenEighths.CenteredMomentFirstDivisorCommonBound.actual_supported_annular_harmonic line 159