OAI/NumberTheory/DirichletL/Moments/GaussEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentGaussEnergy.gaussRow line 13
2. theorem OAI.SevenEighths.CenteredMomentGaussEnergy.gaussRow_pair_summable line 17
3. def OAI.SevenEighths.CenteredMomentGaussEnergy.gaussPolynomial line 34
4. def OAI.SevenEighths.CenteredMomentGaussEnergy.gaussEnergy line 38
5. theorem OAI.SevenEighths.CenteredMomentGaussEnergy.gaussPolynomial_norm_sq line 44
6. theorem OAI.SevenEighths.CenteredMomentGaussEnergy.gaussEnergy_expand line 59
7. theorem OAI.SevenEighths.CenteredMomentGaussEnergy.gaussEnergy_summable line 76
8. theorem OAI.SevenEighths.CenteredMomentGaussEnergy.finite_energy_le_gaussEnergy line 88
9. theorem OAI.SevenEighths.CenteredMomentGaussEnergy.gaussEnergy_poisson line 106