OAI/NumberTheory/Ostmann/QuadraticCenter/PrimeProductMomentScalesAlgebra.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.QuadraticCenter.moment_pow_exp line 8
2. theorem OAI.Ostmann.QuadraticCenter.primeMoment_factorial_sampling_le line 14
3. theorem OAI.Ostmann.QuadraticCenter.sampling_ratio_le line 21
4. theorem OAI.Ostmann.QuadraticCenter.primeMoment_square_coefficient_le line 30
5. theorem OAI.Ostmann.QuadraticCenter.primeMoment_sampling_exp_le line 93
6. theorem OAI.Ostmann.QuadraticCenter.primeMoment_nonsquare_coefficient_le line 115