OAI/NumberTheory/Ostmann/Quadratic/QuadraticSieveInitial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The initial exponent for the quadratic large sieve

The proved additive large sieve and quadratic reciprocity give the starting exponent two in Heath-Brown's iteration, with an absolute constant.

  1. theorem OAI.Ostmann.quadraticSieveBound_initial line 14