OAI/NumberTheory/Ostmann/ZeroDensity/PrimePartialSummation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Partial summation for the reciprocal-prime progression measure

This is the bridge from the published theta estimate (Montgomery--Vaughan, Corollary 11.20, equations (11.32) and (11.34)) to the interval weights used in Section 8. The conversion itself is proved here.

  1. def OAI.Ostmann.primeProgressionLog line 22
  2. def OAI.Ostmann.primeProgressionTheta line 25
  3. def OAI.Ostmann.reciprocalPrimeInterval line 28
  4. def OAI.Ostmann.primeHarmonicWeight line 32
  5. def OAI.Ostmann.primeHarmonicDerivative line 34
  6. theorem OAI.Ostmann.hasDerivAt_primeHarmonicWeight line 37
  7. theorem OAI.Ostmann.continuousOn_primeHarmonicDerivative line 48
  8. theorem OAI.Ostmann.reciprocalPrimeInterval_eq_partialSummation line 60

    Source documentation

    The exact Abel formula on the actual prime progression, with arbitrary real endpoints greater than one.

    theorem reciprocalPrimeInterval_eq_partialSummation (q a : ℕ)
    {u v : ℝ} (hu : 1 < u) (huv : u ≤ v) :
    reciprocalPrimeInterval q a u v =
      primeHarmonicWeight v * primeProgressionTheta q a v -
      primeHarmonicWeight u * primeProgressionTheta q a u -
        ∫ t in Set.Ioc u v, primeHarmonicDerivative t * primeProgressionTheta q a t := by
…

    Mentions: OAI.Ostmann.reciprocalPrimeInterval, OAI.Ostmann.primeHarmonicWeight, OAI.Ostmann.primeProgressionTheta, OAI.Ostmann.primeHarmonicDerivative