OAI/NumberTheory/Ostmann/ZeroDensity/SmoothDirichletIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The initial vertical-line formula for the smooth Mangoldt sum

  1. def OAI.Ostmann.characterVerticalTerm line 12
  2. theorem OAI.Ostmann.characterVerticalTerm_norm line 16
  3. theorem OAI.Ostmann.characterVerticalTerm_integrable line 21
  4. theorem OAI.Ostmann.characterVerticalTerm_summable_norm line 29
  5. theorem OAI.Ostmann.smoothMangoldtMean_eq_vertical_LSeries line 38
  6. theorem OAI.Ostmann.PrimitiveComplexCharacter.mangoldt_LSeries_eq line 64
  7. theorem OAI.Ostmann.smoothMangoldtMean_eq_vertical_logDerivative line 75

    Source documentation

    The exact starting contour for the published explicit formula.

    theorem smoothMangoldtMean_eq_vertical_logDerivative (χ : PrimitiveComplexCharacter)
    (X : ℝ) (hX : 0 < X) :
    smoothMangoldtMean χ.modulus χ.character X =
      ((1 / (2 * Real.pi) : ℝ) : ℂ) * ∫ t : ℝ,
        (-deriv χ.L (primeMellinLine t) / χ.L (primeMellinLine t)) *
          primeVerticalWeight X t := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.smoothMangoldtMean, OAI.Ostmann.primeMellinLine, OAI.Ostmann.primeVerticalWeight