OAI/NumberTheory/TwoPoint/Fourier/ModFiveSmoothedContour.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite quantitative contour bound for the actual smoothed twisted Mangoldt sums, using the zero-free region and the inverse-square tail estimate.

  1. lemma OAI.TwoPointCorrelations.modFive_perron_normalization line 13

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveSmoothedContour.lean:13 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.modFive_smoothed_contour_bound line 19

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveSmoothedContour.lean:19 (same declaration text).