OAI/NumberTheory/DirichletL/Moments/FirstReduced.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFirstReduced.tripleRow line 15
2. def OAI.SevenEighths.CenteredMomentFirstReduced.tripleResidue line 19
3. theorem OAI.SevenEighths.CenteredMomentFirstReduced.tripleResidue_mk line 25
4. theorem OAI.SevenEighths.CenteredMomentFirstReduced.tripleRow_mul line 30
5. def OAI.SevenEighths.CenteredMomentFirstReduced.tripleFourier line 37
6. theorem OAI.SevenEighths.CenteredMomentFirstReduced.tripleRow_radial_summable line 43
7. theorem OAI.SevenEighths.CenteredMomentFirstReduced.tripleRow_poisson line 53
8. theorem OAI.SevenEighths.CenteredMomentFirstReduced.masked_triple_poisson line 66
9. theorem OAI.SevenEighths.CenteredMomentFirstReduced.principalSexticRow_mul line 86
10. theorem OAI.SevenEighths.CenteredMomentFirstReduced.common_residual_reduced_poisson line 98