OAI/NumberTheory/Jacobsthal/Sieve/PrincipalEulerCorrection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.localEulerFactor line 13
2. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.prime_cpow_neg_norm_le_half line 16
3. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.localEulerFactor_ne_zero line 25
4. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.localEulerFactor_differentiable line 35
5. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.localEulerFactor_deriv line 40
6. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_logDeriv_localEulerFactor line 50
7. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.sum_log_primeFactors_le_log line 68
8. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_euler_log_correction_le_log line 78
9. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.modulusEulerProduct line 99
10. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.principal_log_derivative_eq line 102
11. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_principal_log_derivative_difference line 126
12. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.principal_neg_real_log_derivative_le line 134