OAI/NumberTheory/TwoPoint/Fourier/ModFiveStripBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full logarithmic-derivative control in a narrower zero-free strip. Jensen counts all nearby zeros, and their proved horizontal separation bounds the entire pole sum, including at bounded height.

  1. theorem OAI.TwoPointCorrelations.modFive_logderiv_strip_bound line 15

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveStripBound.lean:15 (same declaration text).