OAI/NumberTheory/Ostmann/ZeroDensity/SmoothVerticalKernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeMellinLine line 14
2. theorem OAI.Ostmann.primeMellinLine_re line 16
3. theorem OAI.Ostmann.primeMellinLine_continuous line 19
4. def OAI.Ostmann.primeVerticalWeight line 23
5. theorem OAI.Ostmann.primeVerticalWeight_continuous line 26
6. theorem OAI.Ostmann.primeVerticalWeight_norm line 33
7. theorem OAI.Ostmann.primeVerticalWeight_integrable line 38
8. def OAI.Ostmann.characterMangoldtCoefficient line 46
9. theorem OAI.Ostmann.characterMangoldtCoefficient_summable line 49
10. theorem OAI.Ostmann.characterMangoldt_term_norm line 53
11. theorem OAI.Ostmann.characterMangoldt_term_continuous line 58
12. theorem OAI.Ostmann.characterMangoldt_term_inversion line 70

    Source documentation

    Termwise inversion, including the zero coefficient at n=0.

    theorem characterMangoldt_term_inversion (χ : PrimitiveComplexCharacter)
        (X : ℝ) (hX : 0 < X) (n : ℕ) :
        ((1 / (2 * Real.pi) : ℝ) : ℂ) *
          (∫ t : ℝ, LSeries.term (characterMangoldtCoefficient χ) (primeMellinLine t) n *
            primeVerticalWeight X t) =
          characterMangoldtCoefficient χ n * (primeMeanTest (n / X) : ℂ) := by
    …

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.characterMangoldtCoefficient, OAI.Ostmann.primeMellinLine, OAI.Ostmann.primeVerticalWeight, OAI.Ostmann.primeMeanTest