OAI/NumberTheory/Jacobsthal/Renewal/DickmanMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.Erdos970Dependency.StandardBoundary.rho_exp_bound line 16
2. theorem OAI.Erdos970.Erdos970Dependency.StandardBoundary.rho_moment_integrable line 30
3. theorem OAI.Erdos970.Erdos970Dependency.StandardBoundary.rho_moment_tendsto_zero line 46
4. theorem OAI.Erdos970.Erdos970Dependency.StandardBoundary.halfline_shift line 58
5. theorem OAI.Erdos970.Erdos970Dependency.StandardBoundary.rho_quotient_integral line 86
6. theorem OAI.Erdos970.Erdos970Dependency.StandardBoundary.rho_first_moment line 105
7. theorem OAI.Erdos970.Erdos970Dependency.StandardBoundary.rho_quadratic_quotient line 158