OAI/NumberTheory/Ostmann/Quadratic/QuadraticBilinearComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The divisor-constrained comparison with concrete selected scales

This is the finite comparison of Heath-Brown (1995), Lemma 10. We retain the explicit number of dyadic bins instead of enlarging the selected scales to hide logarithms. All quadratic matrix bounds are at the actual shorter ranges.

  1. theorem OAI.Ostmann.quadratic_dyadic_divisor_mass_bound line 16
  2. theorem OAI.Ostmann.quadratic_bilinear_comparison line 33
  3. theorem OAI.Ostmann.quadratic_bilinear_comparison_epsilon line 54