OAI/NumberTheory/Ostmann/Arithmetic/PrimeProgression.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.PrimeProgression.logPrimeSupport line 9
2. theorem OAI.Ostmann.Arithmetic.PrimeProgression.mem_logPrimeSupport line 14
3. def OAI.Ostmann.Arithmetic.PrimeProgression.harmonicProgression line 20
4. def OAI.Ostmann.Arithmetic.PrimeProgression.harmonicIntegral line 23
5. def OAI.Ostmann.Arithmetic.PrimeProgression.correctedIntegral line 26
6. theorem OAI.Ostmann.Arithmetic.PrimeProgression.sum_harmonicProgression line 30
7. theorem OAI.Ostmann.Arithmetic.PrimeProgression.harmonicProgression_nonneg line 36
8. theorem OAI.Ostmann.Arithmetic.PrimeProgression.deletion_error line 40