OAI/NumberTheory/Jacobsthal/Sieve/LargeModulusSiegelWalfisz.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.cubeHeight line 13
2. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.cubeHeight_pos line 15
3. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.cubeHeight_pow_three line 18
4. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.cubeHeight_mono line 23
5. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.cubeHeight_tendsto line 26
6. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.eventually_polynomial_le_exp line 29
7. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exponential_height_bound line 40
8. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exponential_left_saving line 56
9. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.eventually_exponential_contour_savings line 83
10. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.riesz_character_exponential line 151
11. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.cubeHeight_le_log line 224
12. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exponential_recovery_scale line 231
13. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exponential_recovery_tail line 267
14. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.sharp_character_exponential line 296
15. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.eventually_polynomial_le_X_exp line 362
16. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.eventually_sqrt_le_X_exp line 380
17. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.eventually_exp_sqrt_log_le line 396
18. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.ordinary_psi_exponential line 425
19. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.principal_difference_exponential line 446
20. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.principal_character_exponential line 465
21. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.all_character_exponential line 490
22. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residuePsi_exponential line 512
23. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueTheta_exponential line 528
24. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.cubeHeight_above_sqrt line 565
25. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.modulus_exponential_above_sqrt line 583
26. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueErrorKernel_exp_upper line 594
27. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.residueErrorKernel_exp_high_integral line 611
28. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.large_modulus_siegel_walfisz_eventually line 641
29. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.large_modulus_siegel_walfisz line 718