OAI/NumberTheory/Ostmann/QuadraticSieveCoprimePoissonLatticeBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticSieve.integerInvSquareMass line 11
2. theorem OAI.Ostmann.QuadraticSieve.summable_integer_inv_sq line 13
3. theorem OAI.Ostmann.QuadraticSieve.integerInvSquareMass_pos line 17
4. theorem OAI.Ostmann.QuadraticSieve.schwartz_restricted_lattice_bound line 23
5. def OAI.Ostmann.QuadraticSieve.nonzeroLattice line 67
6. def OAI.Ostmann.QuadraticSieve.latticeTail line 70
7. theorem OAI.Ostmann.QuadraticSieve.nonzeroLattice_bound line 73
8. theorem OAI.Ostmann.QuadraticSieve.latticeTail_bound line 87