OAI/NumberTheory/TwoPointCorrelations/ModFivePerronSeries.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Absolute interchange for the triangular Perron kernel. The estimate is proved for any absolutely convergent Dirichlet series and then specialized to the actual twisted von Mangoldt series.

  1. lemma OAI.TwoPointCorrelations.modFivePerron_term_kernel line 15

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronSeries.lean:15 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFivePerron_term_integrable line 25

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronSeries.lean:25 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFivePerron_term_norm line 36

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronSeries.lean:36 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.modFivePerron_series_interchange line 45

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronSeries.lean:45 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.modFivePerron_term_value line 64

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronSeries.lean:64 (same declaration text).