OAI/NumberTheory/Jacobsthal/Probability/RieszKernelBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszKernel_norm_bound line 14
2. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszMajorant_integrable line 36
3. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.continuous_rieszKernel_line line 39
4. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.integrable_rieszKernel_line line 54
5. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.integral_norm_rieszKernel_line_le line 59
6. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.riesz_mellin_inversion line 66