OAI/NumberTheory/Ostmann/QuadraticSievePoissonLattice.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.QuadraticSieve.schwartz_summable_translateline 8 - theorem
OAI.Ostmann.QuadraticSieve.residue_lattice_summableline 15 - theorem
OAI.Ostmann.QuadraticSieve.integer_lattice_eq_residue_sumline 23 - theorem
OAI.Ostmann.QuadraticSieve.periodic_weighted_poissonline 49