OAI/NumberTheory/CubicMoment/Estimates/MontgomeryVaughanProof.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The required ordinary mean value bound, proved by a Gaussian majorant.

  1. def OAI.CubicFirstMoment.ordinaryMeanValueConstant line 11
  2. lemma OAI.CubicFirstMoment.integerNormPolynomial_continuous line 14
  3. lemma OAI.CubicFirstMoment.gaussian_interval_majorant line 19
  4. lemma OAI.CubicFirstMoment.integerNormPolynomial_translate line 56
  5. lemma OAI.CubicFirstMoment.ordinaryMeanValueConstant_pos line 65
  6. theorem OAI.CubicFirstMoment.montgomeryVaughanBound_proved line 71

    Source documentation

    The ordinary Dirichlet-polynomial mean-square bound.

    theorem montgomeryVaughanBound_proved : MontgomeryVaughanBound ordinaryMeanValueConstant := by
…

    Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.ordinaryMeanValueConstant