OAI/NumberTheory/SiegelZeros/Estimates/PrimeBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.W08.primesUpTo line 11
2. def OAI.SiegelZeros.W08.primeLogMass line 14
3. theorem OAI.SiegelZeros.W08.sum_prime_log_eq_theta line 17
4. theorem OAI.SiegelZeros.W08.sum_prime_log_le line 20
5. theorem OAI.SiegelZeros.W08.sum_selected_prime_log_le line 24
6. theorem OAI.SiegelZeros.W08.sum_prime_divisor_mass_le_log line 32
7. theorem OAI.SiegelZeros.W08.sum_primeFactors_mass_le_log line 51
8. theorem OAI.SiegelZeros.W08.replace_chebyshev_error line 57