OAI/NumberTheory/Ostmann/Quadratic/QuadraticSieveAdditiveStart.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The initial quadratic-sieve bound from the proved additive large sieve

  1. theorem OAI.Ostmann.sum_interval_extension line 14
  2. def OAI.Ostmann.quadraticArray line 25
  3. theorem OAI.Ostmann.quadraticArray_energy line 28
  4. theorem OAI.Ostmann.quadraticArray_character_sum line 35
  5. theorem OAI.Ostmann.quadraticSieveBound_additive line 45