OAI/NumberTheory/Ostmann/QuadraticSieveCoprimePoissonTruncation.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.QuadraticSieve.nonzeroIntegerCutoffline 10 - theorem
OAI.Ostmann.QuadraticSieve.mem_nonzeroIntegerCutoffline 13 - theorem
OAI.Ostmann.QuadraticSieve.tsum_eq_zero_add_trunc_add_tailline 18 - theorem
OAI.Ostmann.QuadraticSieve.schwartz_fourier_zero_eq_integralline 48 - theorem
OAI.Ostmann.QuadraticSieve.schwartz_lattice_eq_zero_add_nonzeroline 52 - theorem
OAI.Ostmann.QuadraticSieve.schwartz_poisson_scaled_truncatedline 59