OAI/NumberTheory/Jacobsthal/Primes/PrimeIntervalFlags.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.intervalPrimes_eq_sdiff line 15
2. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.intervalPrimes_count_sub line 29
3. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.inv_log_intervalIntegrable line 38
4. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.logarithmicIntegral_sub line 46
5. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.logarithmicIntegral_sub_lower line 53
6. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.ordinary_prime_count_exponential line 76
7. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.prime_interval_lower_of_errors line 89
8. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exponential_log_cube_tendsto line 110
9. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.cubeHeight_lower_of_exp_cube line 115
10. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.moving_prime_interval_error_budget line 138
11. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.eventually_interval_polynomial_budget line 190
12. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.moving_prime_interval_lower line 217
13. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.primeIntervalFlags line 264
14. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.mem_primeIntervalFlags line 269
15. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.primeIntervalFlags_lower_card line 284
16. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.primeIntervalFlags_upper_card line 308
17. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.primeIntervalFlags_card_difference line 334
18. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.moving_prime_interval_lower_flags line 345