OAI/NumberTheory/Ostmann/Quadratic/QuadraticComparisonEnvelope.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The numerical minimum in the first recursive quadratic comparison

Here P is the product of the two selected divisor scales and Y is B to the current sieve exponent. This is the three-term calculation in Heath-Brown, section 8, equations (19)--(20).

  1. theorem OAI.Ostmann.quadratic_comparison_prefactor line 15
  2. theorem OAI.Ostmann.quadratic_comparison_envelope line 35