OAI/NumberTheory/TwoPointCorrelations/ModFiveContourRegion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A common closed zero-free rectangle and its uniform logarithmic- derivative bound. This prepares the finite contour shift without a height-dependent analyticity assumption.

  1. theorem OAI.TwoPointCorrelations.modFive_logderiv_rectangles line 15

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

  2. lemma OAI.TwoPointCorrelations.modFive_logderiv_differentiableAt line 43

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveContourRegion.lean:43 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFive_perron_integrand_differentiableAt line 50

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveContourRegion.lean:50 (same declaration text).