OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/FourierSeries.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryDirichletMeanSquare.fourierSeries line 18
2. lemma OAI.OrdinaryDirichletMeanSquare.fourier_summable line 21
3. lemma OAI.OrdinaryDirichletMeanSquare.continuous_fourierSeries line 26
4. lemma OAI.OrdinaryDirichletMeanSquare.gaussian_series_integrable line 32
5. theorem OAI.OrdinaryDirichletMeanSquare.gaussian_series_energy line 48
6. lemma OAI.OrdinaryDirichletMeanSquare.mangoldt_coefficient_summable line 77
7. lemma OAI.OrdinaryDirichletMeanSquare.mangoldt_polynomial_erase_zero line 94
8. theorem OAI.OrdinaryDirichletMeanSquare.mangoldt_series_gaussian_energy line 103