OAI/NumberTheory/Ostmann/QuadraticSieveSmoothed.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.QuadraticSieve.summable_weighted_jacobiline 9 - theorem
OAI.Ostmann.QuadraticSieve.schwartz_summable_scaledline 15 - theorem
OAI.Ostmann.QuadraticSieve.jacobi_sum_norm_sqline 20 - theorem
OAI.Ostmann.QuadraticSieve.weighted_jacobi_energy_expandline 37 - theorem
OAI.Ostmann.QuadraticSieve.schwartz_jacobi_energy_expandline 66