OAI/NumberTheory/Jacobsthal/Primes/UniformDirichletBasepoint.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_LFunction_modulus_height line 16
2. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_LFunction_height_envelope line 43
3. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_LFunction_half_strip line 51
4. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.LFunction_ne_zero_right line 68
5. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.uniform_log_derivative_right line 73
6. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.perronPoint line 85
7. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.perronPoint_re line 88
8. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.perronPoint_re_gt_one line 91
9. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.LFunction_ne_zero_perron_line line 96
10. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.uniform_log_derivative_perron_line line 101
11. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.absoluteZetaTwo line 121
12. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.absoluteZetaTwo_summable line 123
13. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.one_le_absoluteZetaTwo line 128
14. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_LSeries_le_absoluteZetaTwo line 132
15. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_LFunction_le_absoluteZetaTwo line 142
16. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_inv_LFunction_le_absoluteZetaTwo line 148
17. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.uniform_basepoint_bounds line 170