OAI/NumberTheory/JointDickman/Amplification/MultiplicativeExponentialInput.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The published multiplicative exponential-sum input

Montgomery--Vaughan, Exponential sums with multiplicative coefficients, Invent. Math. 43 (1977), Corollary 1, DOI 10.1007/BF01390204. We need only real, everywhere 1-bounded multiplicative coefficients. These satisfy both hypotheses of the published theorem: the prime bound and the sum of squares bound. The uniform constant is independent of the coefficient, hence also of the moving finite set of excluded primes.

  1. def OAI.JointDickman.PublishedInputs.MultiplicativeExponentialInput line 21

    Source documentation

    The finite partial-sum specialization of Montgomery--Vaughan Cor. 1.

    def MultiplicativeExponentialInput : Prop :=
…
  2. theorem OAI.JointDickman.roughSquarefreeWeight_half_bounded line 32
  3. theorem OAI.JointDickman.roughSquarefreeWeight_half_square_sum line 40
  4. theorem OAI.JointDickman.rough_exponential_partial_sum_bound line 50