OAI/NumberTheory/TwoPointCorrelations/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. All analytic hypotheses have been discharged in the preceding zero-free-region and tail lemmas.

  1. lemma OAI.TwoPointCorrelations.modFive_perron_normalization line 13

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

  2. theorem OAI.TwoPointCorrelations.modFive_smoothed_contour_bound line 19

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