OAI/NumberTheory/Ostmann/ZeroDensity/SmoothExplicitIdentity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.smooth_explicit_identity line 14

   Source documentation

   The exact contour remainder. A faithful numbering of the actual zero multiplicities is the only enumeration data used in the formula.

   theorem smooth_explicit_identity (e : ∀ χ, ℕ ≃ CharacterZeroCopy χ)
       (χ : PrimitiveComplexCharacter) (X : ℝ) (hX : 2 ≤ X) :
       smoothMangoldtMean χ.modulus χ.character X +
         (∑' i, smoothZeroTerm (fun ψ => characterZeroEnumeration ψ (e ψ)) χ X i) +
         smoothTrivialZeroTerm χ =
         ((1 / (2 * Real.pi) : ℝ) : ℂ) * ∫ y : ℝ, leftContourIntegrand χ X y := by
   …

   Mentions: OAI.Ostmann.CharacterZeroCopy, OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.smoothMangoldtMean, OAI.Ostmann.smoothZeroTerm, OAI.Ostmann.characterZeroEnumeration, OAI.Ostmann.smoothTrivialZeroTerm, OAI.Ostmann.leftContourIntegrand