OAI/NumberTheory/Ostmann/Quadratic/QuadraticUniformPoisson.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform power-saving coprime Poisson summation

This proves the concrete Schwartz-function form of Heath-Brown (1995), Lemma 13, needed in the two quadratic-sieve error estimates.

  1. theorem OAI.Ostmann.quadratic_uniform_coprime_poisson line 15