OAI/NumberTheory/TwoPoint/Fourier/ModFivePerronShift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative finite contour shift for the actual twisted Mangoldt integrand. The left side stays inside the proved zero-free rectangle and the two horizontal sides are bounded explicitly.

  1. def OAI.TwoPointCorrelations.modFivePerronIntegrand line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFivePerronShift.lean:14 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.modFive_finite_perron_shift line 19

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