OAI/NumberTheory/Ostmann/Quadratic/QuadraticBiasSmallness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform smallness of translated quadratic biases

The residue partition is fixed before the error tolerance. The proof constructs both prime blocks, all integer parameters and the positive and reflected tails.

  1. theorem OAI.Ostmann.eventual_small_prime_separation line 18
  2. theorem OAI.Ostmann.eventual_translated_quadratic_bias_lt line 28