OAI/NumberTheory/Ostmann/Preliminaries/PrimeLogReciprocal.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Preliminaries.primeLogWeight line 12
2. lemma OAI.Ostmann.Preliminaries.primeLogWeight_nonneg line 15
3. lemma OAI.Ostmann.Preliminaries.sum_primeLogWeight line 21
4. lemma OAI.Ostmann.Preliminaries.sum_primeLogWeight_le line 28
5. def OAI.Ostmann.Preliminaries.primeLogReciprocalConstant line 35
6. lemma OAI.Ostmann.Preliminaries.primeLogReciprocalConstant_pos line 38
7. lemma OAI.Ostmann.Preliminaries.sum_primeLogWeight_le_mul_log line 44
8. def OAI.Ostmann.Preliminaries.inverseLogSquare line 58
9. lemma OAI.Ostmann.Preliminaries.inverseLogSquare_hasDerivAt line 60
10. lemma OAI.Ostmann.Preliminaries.inverseLogSquare_deriv line 68
11. lemma OAI.Ostmann.Preliminaries.inverseLogSquare_deriv_integrable line 72
12. lemma OAI.Ostmann.Preliminaries.sum_primeLog_inverseLogSquare line 85
13. def OAI.Ostmann.Preliminaries.primeLogReciprocalMajorant line 101
14. lemma OAI.Ostmann.Preliminaries.primeLogReciprocalMajorant_nonneg line 104
15. lemma OAI.Ostmann.Preliminaries.primeLogReciprocalMajorant_integrable line 111
16. lemma OAI.Ostmann.Preliminaries.primeLogReciprocal_abel_bound line 118
17. theorem OAI.Ostmann.Preliminaries.prime_log_reciprocal_sum_bounded line 174