OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/LogBin.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryDirichletMeanSquare.logBin line 18
2. def OAI.OrdinaryDirichletMeanSquare.mangoldtCoefficient line 20
3. def OAI.OrdinaryDirichletMeanSquare.chebyshevConstant line 23
4. lemma OAI.OrdinaryDirichletMeanSquare.chebyshevConstant_pos line 25
5. lemma OAI.OrdinaryDirichletMeanSquare.logBin_bounds line 30
6. lemma OAI.OrdinaryDirichletMeanSquare.logBin_close line 34
7. lemma OAI.OrdinaryDirichletMeanSquare.mangoldt_coefficient_bound line 39
8. lemma OAI.OrdinaryDirichletMeanSquare.mangoldt_bin_mass line 49
9. theorem OAI.OrdinaryDirichletMeanSquare.mangoldt_gaussian_energy line 89