OAI/NumberTheory/Jacobsthal/Sieve/ResidueSqrtSplit.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residuePsi line 16
2. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residuePsi_character_sum line 19
3. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residuePsi_error_le line 37
4. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residuePsi_log_power line 87
5. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residuePrimeWeight line 112
6. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueTheta line 115
7. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residuePrimeWeight_eq line 118
8. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residuePsi_sub_theta_bounds line 128
9. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.eventually_sqrt_le_log_power line 149
10. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueTheta_log_power line 164
11. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.intervalPrimes_zero_eq line 202
12. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.intervalPrimes_card_eq_sum_weight line 218
13. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueTheta_kernel_integrable line 233
14. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.intervalPrimes_card_eq_theta line 243
15. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueErrorKernel line 280
16. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueErrorKernel_integrable line 283
17. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueErrorKernel_eq line 290
18. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.intervalPrimes_error_eq line 295
19. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueTheta_nonneg line 316
20. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueTheta_le_theta line 324
21. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueErrorKernel_coarse line 336
22. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueErrorKernel_low_integral line 358
23. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.modulus_admissible_above_sqrt line 377
24. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueErrorKernel_upper_bound line 398
25. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueErrorKernel_high_integral line 431