OAI/NumberTheory/Jacobsthal/Primes/RieszMellinKernel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.modulusHeight_diskPoint_le line 12
2. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exists_uniform_zero_separation line 33
3. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exists_uniform_nonprincipal_strip_bound line 93
4. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszWeight line 171
5. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszProfile line 172
6. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszKernel line 175
7. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszProfile_eq_weight line 177
8. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.continuous_rieszWeight line 185
9. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.continuousAt_rieszProfile line 187
10. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.hasMellin_rieszProfile line 193
11. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszWeight_nonneg line 214
12. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszWeight_le_one line 215
13. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszWeight_eq_zero line 218