OAI/NumberTheory/Ostmann/Preliminaries/PublishedAdditiveSieve.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The classical additive large-sieve input

H. L. Montgomery and R. C. Vaughan, The large sieve, Mathematika 20 (1973), 119–134, Theorem 1. The separated-frequency inequality gives the constant M - 1 + Q^2 on reduced fractions of denominator at most Q; below it is weakened to M + Q^2. This is exactly the finite-interval specialization (2.1) stated in the assigned manuscript, and applies to arbitrary complex coefficients.

  1. def OAI.Ostmann.sieveAdditivePhase line 19
  2. def OAI.Ostmann.reducedNumerators line 22
  3. def OAI.Ostmann.additiveSieveSum line 25
  4. def OAI.Ostmann.PublishedAdditiveLargeSieve line 30

    Source documentation

    The additive large sieve for separated frequencies and arbitrary complex coefficients.

    def PublishedAdditiveLargeSieve : Prop :=
…